YELLOW13

:: Introduction to Meet-Continuous Topological Lattices
::  by Artur Korni{\l}owicz
::
:: Received November 3, 1998
:: Copyright (c) 1998-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies STRUCT_0, XBOOLE_0, ZFMISC_1, ORDERS_2, WAYBEL_9, PRE_TOPC,
      FINSET_1, SUBSET_1, RCOMP_1, TARSKI, NATTRA_1, CARD_5, RELAT_2, FUNCT_1,
      WAYBEL_0, RELAT_1, SEQM_3, XXREAL_0, YELLOW_2, YELLOW_1, CARD_FIL,
      ORDINAL2, WELLORD1, WAYBEL_1, FUNCT_2, REWRITE1, LATTICES, YELLOW_0,
      LATTICE3, TDLAT_3, RLVECT_3, SETFAM_1, YELLOW_8, TOPS_1, CONNSP_2,
      PRELAMB, CANTOR_1, WAYBEL_2, YELLOW13, CARD_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, TOPS_2, FUNCT_1, RELSET_1,
      BINOP_1, FUNCT_2, FINSET_1, SETFAM_1, DOMAIN_1, STRUCT_0, ORDERS_2,
      PRE_TOPC, TOPS_1, COMPTS_1, TDLAT_2, TDLAT_3, LATTICE3, CANTOR_1,
      CONNSP_2, BORSUK_1, YELLOW_0, WAYBEL_0, YELLOW_1, ORDERS_3, WAYBEL_1,
      YELLOW_2, YELLOW_3, WAYBEL_2, YELLOW_8, WAYBEL_9;
 constructors SETFAM_1, TOPS_1, BORSUK_1, URYSOHN1, LATTICE3, TDLAT_2, TDLAT_3,
      T_0TOPSP, CANTOR_1, ORDERS_3, WAYBEL_1, WAYBEL_9, YELLOW_8, COMPTS_1,
      TOPS_2, WAYBEL_2;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, PRE_TOPC,
      TOPS_1, BORSUK_1, LATTICE3, YELLOW_0, TDLAT_3, TEX_1, WAYBEL_0, YELLOW_1,
      YELLOW_2, WAYBEL_1, WAYBEL_3, YELLOW_9, YELLOW11, YELLOW12, RELAT_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, LATTICE3, PRE_TOPC, TOPS_2, WAYBEL_0, WAYBEL_1, YELLOW_8,
      BORSUK_1, XBOOLE_0, COMPTS_1;
 equalities STRUCT_0, SUBSET_1, BINOP_1;
 expansions TARSKI, LATTICE3, PRE_TOPC, BORSUK_1, XBOOLE_0, COMPTS_1;
 theorems TARSKI, PRE_TOPC, ORDERS_2, TOPS_1, WAYBEL_3, CONNSP_2, TDLAT_3,
      SETFAM_1, COMPTS_1, CANTOR_1, ZFMISC_1, YELLOW_0, YELLOW_2, YELLOW_3,
      YELLOW_8, WAYBEL_1, WAYBEL14, YELLOW_9, URYSOHN1, YELLOW_4, WAYBEL_0,
      RELAT_1, TDLAT_2, FUNCT_1, FUNCT_2, ORDERS_3, BORSUK_1, TEX_1, WAYBEL_2,
      XBOOLE_0, XBOOLE_1, SUBSET_1, TOPS_2;
 schemes FINSET_1;

begin  :: Preliminaries

theorem Th1:
  for T being T_1 non empty TopSpace, A being finite Subset of T
  holds A is closed
proof
  let T be T_1 non empty TopSpace, A be finite Subset of T;
  defpred P[set] means ex S being Subset of T st $1 = S & S is closed;
A1: P[{}]
  proof
    take {}T;
    thus {}T = {};
    thus thesis;
  end;
A2: for x, C being set st x in A & C c= A & P[C] holds P[C \/ {x}]
  proof
    let x, C be set;
    assume that
A3: x in A and
    C c= A and
A4: P[C];
    reconsider y = x as Element of T by A3;
    consider S being Subset of T such that
A5: C = S and
A6: S is closed by A4;
    {y} is closed by URYSOHN1:19;
    then S \/ {y} is closed by A6;
    hence thesis by A5;
  end;
A7: A is finite;
  P[A] from FINSET_1:sch 2(A7,A1,A2);
  hence thesis;
end;

registration
  let T be T_1 non empty TopSpace;
  cluster finite -> closed for Subset of T;
  coherence by Th1;
end;

registration
  let T be compact TopStruct;
  cluster [#]T -> compact;
  coherence by COMPTS_1:1;
end;

registration
  cluster finite T_1 -> discrete for non empty TopSpace;
  coherence
  proof
    let T be non empty TopSpace;
    assume T is finite T_1;
    then for A being Subset of T holds A is closed;
    hence thesis by TDLAT_3:16;
  end;
end;

registration
  cluster finite -> compact for TopSpace;
  coherence;
end;

theorem Th2:
  for T being discrete non empty TopSpace holds T is normal
proof
  let T be discrete non empty TopSpace;
  let W, V be Subset of T such that
  W <> {} and
  V <> {} and
  W is closed and
  V is closed and
A1: W /\ V = {};
  take P = W, Q = V;
  thus P is open & Q is open by TDLAT_3:15;
  thus W c= P & V c= Q & P /\ Q = {} by A1;
end;

theorem Th3:
  for T being discrete non empty TopSpace holds T is regular
proof
  let T be discrete non empty TopSpace;
  let p be Point of T, P be Subset of T such that
  P <> {} and
  P is closed and
A1: p in P`;
  take W = {p}, V = P;
  thus W is open & V is open by TDLAT_3:15;
A2: not p in P by A1,XBOOLE_0:def 5;
  W /\ V c= {}
  proof
    let a be object;
    assume
A3: a in W /\ V;
    assume not a in {};
    a in W & a in V by A3,XBOOLE_0:def 4;
    hence contradiction by A2,TARSKI:def 1;
  end;
  hence p in W & P c= V & W /\ V = {} by TARSKI:def 1;
end;

theorem Th4:
  for T being discrete non empty TopSpace holds T is T_2
proof
  let T be discrete non empty TopSpace;
  let p, q be Point of T such that
A1: not p = q;
  take W = {p}, V = {q};
  thus W is open & V is open by TDLAT_3:15;
  W /\ V c= {}
  proof
    let a be object;
    assume
A2: a in W /\ V;
    then a in W by XBOOLE_0:def 4;
    then
A3: a = p by TARSKI:def 1;
    assume not a in {};
    a in V by A2,XBOOLE_0:def 4;
    hence contradiction by A1,A3,TARSKI:def 1;
  end;
  hence p in W & q in V & W /\ V = {} by TARSKI:def 1;
end;

theorem Th5:
  for T being discrete non empty TopSpace holds T is T_1
proof
  let T be discrete non empty TopSpace;
  for p being Point of T holds {p} is closed by TDLAT_3:16;
  hence thesis by URYSOHN1:19;
end;

registration
  cluster discrete non empty -> normal regular T_2 T_1 for TopSpace;
  coherence by Th2,Th3,Th4,Th5;
end;

registration
  cluster T_4 -> regular for non empty TopSpace;
  coherence
  proof
    let T be non empty TopSpace such that
A1: T is T_4;
    let p be Point of T, P be Subset of T such that
A2: P <> {} & P is closed and
A3: p in P`;
A4: not p in P by A3,XBOOLE_0:def 5;
    P /\ {p} c= {}
    proof
      let a be object;
      assume
A5:   a in P /\ {p};
      assume not a in {};
      a in P & a in {p} by A5,XBOOLE_0:def 4;
      hence contradiction by A4,TARSKI:def 1;
    end;
    then P /\ {p} = {};
    then P misses {p};
    then consider R, Q being Subset of T such that
A6: R is open & Q is open & {p} c= R & P c= Q & R misses Q by A1,A2,
COMPTS_1:def 3;
    take R, Q;
    p in {p} by TARSKI:def 1;
    hence thesis by A6;
  end;
end;

registration
  cluster T_3 -> T_2 for TopSpace;
  coherence
  proof
    let T be TopSpace such that
A1: T is T_3;
    let p, q be Point of T;
    assume
A2: p <> q;
    then
A3: not p in {q} by TARSKI:def 1;
    now
      assume
A4:   the carrier of T = {};
      then p = {} by SUBSET_1:def 1;
      hence contradiction by A2,A4,SUBSET_1:def 1;
    end;
    then reconsider T9 = T as non empty TopSpace;
    reconsider p,q as Point of T9;
    p in {q}` by A3,SUBSET_1:29;
    then consider W, V being Subset of T such that
A5: W is open & V is open & p in W & {q} c= V & W misses V by A1,COMPTS_1:def 2
;
    take W, V;
    q in {q} by TARSKI:def 1;
    hence thesis by A5;
  end;
end;

theorem Th6:
  for S being reflexive RelStr, T being reflexive transitive RelStr
  , f being Function of S, T, X being Subset of S holds downarrow (f.:X) c=
  downarrow (f.:downarrow X)
proof
  let S be reflexive RelStr, T be reflexive transitive RelStr, f be Function
  of S, T, X be Subset of S;
  f.:X c= f.:downarrow X by RELAT_1:123,WAYBEL_0:16;
  hence thesis by YELLOW_3:6;
end;

theorem
  for S being reflexive RelStr, T being reflexive transitive RelStr, f
being Function of S, T, X being Subset of S st f is monotone holds downarrow (f
  .:X) = downarrow (f.:downarrow X)
proof
  let S be reflexive RelStr, T be reflexive transitive RelStr, f be Function
  of S, T, X be Subset of S such that
A1: f is monotone;
  thus downarrow f.:X c= downarrow f.:downarrow X by Th6;
  let a be object;
  assume
A2: a in downarrow (f.:downarrow X);
  then reconsider T1 = T as non empty reflexive transitive RelStr;
  reconsider b = a as Element of T1 by A2;
  consider fx being Element of T1 such that
A3: fx >= b and
A4: fx in f.:downarrow X by A2,WAYBEL_0:def 15;
  consider x being object such that
A5: x in dom f and
A6: x in downarrow X and
A7: fx = f.x by A4,FUNCT_1:def 6;
  reconsider S1 = S as non empty reflexive RelStr by A5;
  reconsider x as Element of S1 by A5;
  consider y being Element of S1 such that
A8: y >= x and
A9: y in X by A6,WAYBEL_0:def 15;
  reconsider f1 = f as Function of S1, T1;
  f1.x <= f1.y by A1,A8,ORDERS_3:def 5;
  then
A10: b <= f1.y by A3,A7,ORDERS_2:3;
  the carrier of T1 <> {};
  then dom f = the carrier of S by FUNCT_2:def 1;
  then f.y in f.:X by A9,FUNCT_1:def 6;
  hence thesis by A10,WAYBEL_0:def 15;
end;

theorem Th8:
  for N being non empty Poset holds IdsMap N is one-to-one
proof
  let N be non empty Poset;
  set f = IdsMap N;
  let x, y be Element of N such that
A1: f.x = f.y;
  f.x = downarrow x & f.y = downarrow y by YELLOW_2:def 4;
  hence thesis by A1,WAYBEL_0:19;
end;

registration
  let N be non empty Poset;
  cluster IdsMap N -> one-to-one;
  coherence by Th8;
end;

theorem Th9:
  for N being finite LATTICE holds SupMap N is one-to-one
proof
  let N be finite LATTICE;
  set f = SupMap N;
  let x, y be Element of InclPoset Ids N such that
A1: f.x = f.y;
  reconsider X = x, Y = y as Ideal of N by YELLOW_2:41;
A2: f.x = sup X & f.y = sup Y by YELLOW_2:def 3;
  X = Y
  proof
    hereby
      let a be object;
A3:   sup Y in Y by WAYBEL_3:16;
      assume
A4:   a in X;
      then reconsider b = a as Element of N;
      b <= sup Y by A1,A2,A4,YELLOW_0:17,YELLOW_4:1;
      hence a in Y by A3,WAYBEL_0:def 19;
    end;
    let a be object;
A5: sup X in X by WAYBEL_3:16;
    assume
A6: a in Y;
    then reconsider b = a as Element of N;
    b <= sup X by A1,A2,A6,YELLOW_0:17,YELLOW_4:1;
    hence thesis by A5,WAYBEL_0:def 19;
  end;
  hence thesis;
end;

registration
  let N be finite LATTICE;
  cluster SupMap N -> one-to-one;
  coherence by Th9;
end;

theorem
  for N being finite LATTICE holds N, InclPoset Ids N are_isomorphic
proof
  let N be finite LATTICE;
  set I = InclPoset Ids N;
  take i = IdsMap N;
  N is non empty & I is non empty implies i is one-to-one monotone & ex s
  being Function of I,N st s = i" & s is monotone
  proof
    assume that
    N is non empty and
    I is non empty;
    thus i is one-to-one monotone;
    take s = SupMap N;
    [i,s] is Galois by WAYBEL_1:57;
    then i is onto by WAYBEL_1:24;
    then
A1: rng i = the carrier of I by FUNCT_2:def 3;
A2: for y, x being object holds y in rng i & x = s.y iff x in dom i & y = i.x
    proof
      let y, x be object;
A3:   dom i = the carrier of N by FUNCT_2:def 1;
      hereby
        assume that
A4:     y in rng i and
A5:     x = s.y;
        reconsider Y = y as Element of I by A4;
        x = s.Y by A5;
        hence x in dom i by A3;
        reconsider Y1 = Y as Ideal of N by YELLOW_2:41;
        thus i.x = i.sup Y1 by A5,YELLOW_2:def 3
          .= downarrow sup Y1 by YELLOW_2:def 4
          .= y by WAYBEL14:5,WAYBEL_3:16;
      end;
      assume that
A6:   x in dom i and
A7:   y = i.x;
      reconsider X = x as Element of N by A6;
A8:   y = i.X by A7;
      then reconsider Y = y as Ideal of N by YELLOW_2:41;
      thus y in rng i by A1,A8;
      thus s.y = sup Y by YELLOW_2:def 3
        .= sup downarrow X by A7,YELLOW_2:def 4
        .= x by WAYBEL_0:34;
    end;
    dom s = the carrier of I by FUNCT_2:def 1;
    hence s = i" by A1,A2,FUNCT_1:32;
    thus thesis;
  end;
  hence thesis by WAYBEL_0:def 38;
end;

theorem Th11:
  for N being complete non empty Poset, x being Element of N, X
  being non empty Subset of N holds x"/\" preserves_inf_of X
proof
  let N be complete non empty Poset, x be Element of N, X be non empty
  Subset of N such that
A1: ex_inf_of X,N;
A2: for b being Element of N st b is_<=_than (x"/\").:X holds x"/\".inf X >= b
  proof
    consider y being object such that
A3: y in X by XBOOLE_0:def 1;
    reconsider y as Element of N by A3;
    let b be Element of N such that
A4: b is_<=_than (x"/\").:X;
A5: (x"/\").: X = {x"/\"z where z is Element of N: z in X} by WAYBEL_1:61;
    then x "/\" y in (x"/\").:X by A3;
    then
A6: b <= x "/\" y by A4;
    X is_>=_than b
    proof
      let c be Element of N;
      assume c in X;
      then x "/\" c in (x"/\").:X by A5;
      then
A7:   b <= x "/\" c by A4;
      x "/\" c <= c by YELLOW_0:23;
      hence b <= c by A7,ORDERS_2:3;
    end;
    then
A8: b <= inf X by A1,YELLOW_0:def 10;
    x "/\" y <= x by YELLOW_0:23;
    then b <= x by A6,ORDERS_2:3;
    then b "/\" b <= x "/\" inf X by A8,YELLOW_3:2;
    then b <= x "/\" inf X by YELLOW_0:25;
    hence b <= x"/\".inf X by WAYBEL_1:def 18;
  end;
  thus ex_inf_of (x"/\").:X,N by YELLOW_0:17;
  inf X is_<=_than X by A1,YELLOW_0:def 10;
  then x"/\".inf X is_<=_than (x"/\").:X by YELLOW_2:13;
  hence thesis by A2,YELLOW_0:33;
end;

theorem Th12:
  for N being complete non empty Poset, x being Element of N
  holds x"/\" is meet-preserving
proof
  let N be complete non empty Poset, x be Element of N;
  let a, b be Element of N;
  thus thesis by Th11;
end;

registration
  let N be complete non empty Poset, x be Element of N;
  cluster x"/\" -> meet-preserving;
  coherence by Th12;
end;

begin  :: On the basis of topological spaces

theorem
  for T being anti-discrete non empty TopStruct, p being Point of T
  holds {the carrier of T} is Basis of p
proof
  let T be anti-discrete non empty TopStruct, p be Point of T;
  set A = {the carrier of T};
  A c= bool the carrier of T
  proof
    let a be object;
    assume a in A;
    then
A1: a = the carrier of T by TARSKI:def 1;
    the carrier of T c= the carrier of T;
    hence thesis by A1;
  end;
  then reconsider A as Subset-Family of T;
  A is Basis of p
  proof
A2: A is open
    proof
      let a be Subset of T;
      assume a in A;
      then a = [#]T by TARSKI:def 1;
      hence thesis;
    end;
    A is p-quasi_basis
    proof
    Intersect A = meet A by SETFAM_1:def 9
      .= the carrier of T by SETFAM_1:10;
    hence p in Intersect A;
    let S be Subset of T;
    assume S is open & p in S;
    then
A3: S = the carrier of T by TDLAT_3:18;
    take S;
    thus thesis by A3,TARSKI:def 1;
    end;
    hence thesis by A2;
  end;
  hence thesis;
end;

theorem
  for T being anti-discrete non empty TopStruct, p being Point of T, D
  being Basis of p holds D = {the carrier of T}
proof
  let T be anti-discrete non empty TopStruct, p be Point of T, D be Basis of p;
  thus D c= {the carrier of T}
  proof
    let a be object;
    assume
A1: a in D;
    then reconsider X = a as Subset of T;
    X is open & p in X by A1,YELLOW_8:12;
    then X = the carrier of T by TDLAT_3:18;
    hence thesis by TARSKI:def 1;
  end;
  hence thesis by ZFMISC_1:33;
end;

theorem
  for T being non empty TopSpace, P being Basis of T, p being Point of T
  holds {A where A is Subset of T: A in P & p in A} is Basis of p
proof
  let T be non empty TopSpace, P be Basis of T, p be Point of T;
  set Z = {A where A is Subset of T: A in P & p in A};
  Z c= bool the carrier of T
  proof
    let z be object;
    assume z in Z;
    then ex A being Subset of T st A = z & A in P & p in A;
    hence thesis;
  end;
  then reconsider Z as Subset-Family of T;
  reconsider Z as Subset-Family of T;
  Z is Basis of p
  proof
A1: Z is open
    proof
      let z be Subset of T;
      assume z in Z;
      then consider A being Subset of T such that
A2:   A = z and
A3:   A in P and
      p in A;
      A is open by A3,YELLOW_8:10;
      hence thesis by A2;
    end;
    Z is p-quasi_basis
    proof
    now
      let z be set;
      assume z in Z;
      then ex A being Subset of T st A = z & A in P & p in A;
      hence p in z;
    end;
    hence p in Intersect Z by SETFAM_1:43;
    let S be Subset of T;
    assume S is open & p in S;
    then consider V being Subset of T such that
A4: V in P & p in V & V c= S by YELLOW_9:31;
    take V;
    thus thesis by A4;
    end;
    hence thesis by A1;
  end;
  hence thesis;
end;

Lm1: for T being non empty TopStruct, A being Subset of T, p being Point of T
st p in Cl A for K being Basis of p, Q being Subset of T st Q in K holds A
meets Q
proof
  let T be non empty TopStruct, A be Subset of T, p be Point of T such that
A1: p in Cl A;
  let K be Basis of p, Q be Subset of T;
  assume Q in K;
  then Q is open & p in Q by YELLOW_8:12;
  then A meets Q by A1,PRE_TOPC:def 7;
  hence A /\ Q <> {};
end;

Lm2: for T being non empty TopStruct, A being Subset of T, p being Point of T
st for K being Basis of p, Q being Subset of T st Q in K holds A meets Q ex K
being Basis of p st for Q being Subset of T st Q in K holds A meets Q
proof
  let T be non empty TopStruct, A be Subset of T, p be Point of T such that
A1: for K being Basis of p, Q being Subset of T st Q in K holds A meets Q and
A2: for K being Basis of p ex Q being Subset of T st Q in K & A misses Q;
  set K = the Basis of p;
  ex Q being Subset of T st Q in K & A misses Q by A2;
  hence contradiction by A1;
end;

Lm3: for T being non empty TopStruct, A being Subset of T, p being Point of T
st ex K being Basis of p st for Q being Subset of T st Q in K holds A meets Q
holds p in Cl A
proof
  let T be non empty TopStruct, A be Subset of T, p be Point of T;
  given K being Basis of p such that
A1: for Q being Subset of T st Q in K holds A meets Q;
  assume not p in Cl A;
  then consider F being Subset of T such that
A2: F is closed and
A3: A c= F and
A4: not p in F by PRE_TOPC:15;
A5: A misses F` by A3,SUBSET_1:24;
  p in F` & F` is open by A2,A4,XBOOLE_0:def 5;
  then consider W being Subset of T such that
A6: W in K and
A7: W c= F` by YELLOW_8:13;
  A meets W by A1,A6;
  hence contradiction by A7,A5,XBOOLE_1:63;
end;

theorem
  for T being non empty TopStruct, A being Subset of T, p being Point of
  T holds p in Cl A iff for K being Basis of p, Q being Subset of T st Q in K
  holds A meets Q
proof
  let T be non empty TopStruct, A be Subset of T, p be Point of T;
  thus p in Cl A implies for K being Basis of p, Q being Subset of T st Q in K
  holds A meets Q by Lm1;
  assume for K being Basis of p, Q being Subset of T st Q in K holds A meets Q;
  then
  ex K being Basis of p st for Q being Subset of T st Q in K holds A meets
  Q by Lm2;
  hence thesis by Lm3;
end;

theorem
  for T being non empty TopStruct, A being Subset of T, p being Point of
T holds p in Cl A iff ex K being Basis of p st for Q being Subset of T st Q in
  K holds A meets Q
proof
  let T be non empty TopStruct, A be Subset of T, p be Point of T;
  hereby
    assume p in Cl A;
    then
    for K being Basis of p, Q being Subset of T st Q in K holds A meets Q
    by Lm1;
    hence ex K being Basis of p st for Q being Subset of T st Q in K holds A
    meets Q by Lm2;
  end;
  assume
  ex K being Basis of p st for Q being Subset of T st Q in K holds A meets Q;
  hence thesis by Lm3;
end;

definition
  let T be TopStruct, p be Point of T;
  mode basis of p -> Subset-Family of T means
    :Def1:
    for A being Subset of T
    st p in Int A ex P being Subset of T st P in it & p in Int P & P c= A;
  existence
  proof
    reconsider F = bool the carrier of T as Subset-Family of T;
    reconsider F as Subset-Family of T;
    take F;
    let A be Subset of T such that
A1: p in Int A;
    take Int A;
    thus thesis by A1,TOPS_1:16;
  end;
end;

definition
  let T be non empty TopSpace, p be Point of T;
  redefine mode basis of p means  :: redefines basis (YELLOW13, definition)
    for A being a_neighborhood of p ex P being
    a_neighborhood of p st P in it & P c= A;
  compatibility
  proof
    let F be Subset-Family of T;
    hereby
      assume
A1:   F is basis of p;
      let A be a_neighborhood of p;
      p in Int A by CONNSP_2:def 1;
      then consider P being Subset of T such that
A2:   P in F and
A3:   p in Int P and
A4:   P c= A by A1,Def1;
      reconsider P as a_neighborhood of p by A3,CONNSP_2:def 1;
      take P;
      thus P in F & P c= A by A2,A4;
    end;
    assume
A5: for A being a_neighborhood of p ex P being a_neighborhood of p st
    P in F & P c= A;
    let A be Subset of T;
    assume p in Int A;
    then A is a_neighborhood of p by CONNSP_2:def 1;
    then consider P being a_neighborhood of p such that
A6: P in F & P c= A by A5;
    take P;
    thus thesis by A6,CONNSP_2:def 1;
  end;
end;

theorem Th18:
  for T being TopStruct, p being Point of T holds bool the carrier
  of T is basis of p
proof
  let T be TopStruct, p be Point of T;
  reconsider F = bool the carrier of T as Subset-Family of T;
  reconsider F as Subset-Family of T;
  F is basis of p
  proof
    let A be Subset of T such that
A1: p in Int A;
    take Int A;
    thus thesis by A1,TOPS_1:16;
  end;
  hence thesis;
end;

theorem Th19:
  for T being non empty TopSpace, p being Point of T, P being
  basis of p holds P is non empty
proof
  let T be non empty TopSpace, p be Point of T, P be basis of p;
  Int [#]T = [#]T by TOPS_1:15;
  then ex W being Subset of T st W in P & p in Int W & W c= [#]T by Def1;
  hence thesis;
end;

registration
  let T be non empty TopSpace, p be Point of T;
  cluster -> non empty for basis of p;
  coherence by Th19;
end;

registration
  let T be TopStruct, p be Point of T;
  cluster non empty for basis of p;
  existence
  proof
    bool the carrier of T is basis of p by Th18;
    hence thesis;
  end;
end;

definition
  let T be TopStruct, p be Point of T, P be basis of p;
  attr P is correct means
  :Def3:
  for A being Subset of T holds A in P iff p in Int A;
end;

Lm4: now
  let T be TopStruct, p be Point of T;
  let K be set such that
A1: K = {A where A is Subset of T: p in Int A};
  K c= bool the carrier of T
  proof
    let y be object;
    assume y in K;
    then ex A being Subset of T st y = A & p in Int A by A1;
    hence thesis;
  end;
  then reconsider J = K as Subset-Family of T;
  reconsider J as Subset-Family of T;
  for A being Subset of T st p in Int A ex P being Subset of T st P in J &
  p in Int P & P c= A
  proof
    let A be Subset of T such that
A2: p in Int A;
    take P = A;
    thus thesis by A1,A2;
  end;
  hence K is basis of p by Def1;
end;

Lm5: now
  let T be TopStruct, p be Point of T, K be basis of p such that
A1: K = {A where A is Subset of T: p in Int A};
  thus K is correct
  proof
    let A be Subset of T;
    hereby
      assume A in K;
      then ex M being Subset of T st A = M & p in Int M by A1;
      hence p in Int A;
    end;
    thus thesis by A1;
  end;
end;

registration
  let T be TopStruct, p be Point of T;
  cluster correct for basis of p;
  existence
  proof
    reconsider P = {A where A is Subset of T: p in Int A} as basis of p by Lm4;
    take P;
    thus thesis by Lm5;
  end;
end;

theorem
  for T being TopStruct, p being Point of T holds {A where A is Subset
  of T: p in Int A} is correct basis of p by Lm4,Lm5;

registration
  let T be non empty TopSpace, p be Point of T;
  cluster non empty correct for basis of p;
  existence
  proof
    reconsider K = {A where A is Subset of T: p in Int A} as correct basis of
    p by Lm4,Lm5;
    take K;
    thus thesis;
  end;
end;

theorem
  for T being anti-discrete non empty TopStruct, p being Point of T
  holds {the carrier of T} is correct basis of p
proof
  let T be anti-discrete non empty TopStruct, p be Point of T;
  set A = {the carrier of T};
  A c= bool the carrier of T
  proof
    let a be object;
    assume a in A;
    then
A1: a = the carrier of T by TARSKI:def 1;
    the carrier of T c= the carrier of T;
    hence thesis by A1;
  end;
  then reconsider A as Subset-Family of T;
  reconsider A as Subset-Family of T;
  A is basis of p
  proof
    let S be a_neighborhood of p;
    take S;
    p in Int S by CONNSP_2:def 1;
    then
A2: Int S = the carrier of T by TDLAT_3:18;
    Int S c= S by TOPS_1:16;
    then Int S = S by A2;
    hence thesis by A2,TARSKI:def 1;
  end;
  then reconsider A as basis of p;
  A is correct
  proof
    let X be Subset of T;
    hereby
      assume X in A;
      then X = the carrier of T by TARSKI:def 1;
      then Int X = [#]T by TOPS_1:15;
      hence p in Int X;
    end;
    assume p in Int X;
    then
A3: Int X = the carrier of T by TDLAT_3:18;
    Int X c= X by TOPS_1:16;
    then Int X = X by A3;
    hence thesis by A3,TARSKI:def 1;
  end;
  hence thesis;
end;

theorem
  for T being anti-discrete non empty TopStruct, p being Point of T, D
  being correct basis of p holds D = {the carrier of T}
proof
  let T be anti-discrete non empty TopStruct, p be Point of T, D be correct
  basis of p;
  thus D c= {the carrier of T}
  proof
    let a be object;
    assume
A1: a in D;
    then reconsider X = a as Subset of T;
    p in Int X by A1,Def3;
    then
A2: Int X = the carrier of T by TDLAT_3:18;
    Int X c= X by TOPS_1:16;
    then Int X = X by A2;
    hence thesis by A2,TARSKI:def 1;
  end;
  hence thesis by ZFMISC_1:33;
end;

theorem
  for T being non empty TopSpace, p being Point of T, P being Basis of p
  holds P is basis of p
proof
  let T be non empty TopSpace, p be Point of T, P be Basis of p;
  now
    let A be Subset of T;
    assume p in Int A;
    then consider V being Subset of T such that
A1: V in P and
A2: V c= Int A by YELLOW_8:def 1;
    take V;
    V is open by A1,YELLOW_8:12;
    then Int A c= A & Int V = V by TOPS_1:16,23;
    hence V in P & p in Int V & V c= A by A1,A2,YELLOW_8:12;
  end;
  hence thesis by Def1;
end;

definition
  let T be TopStruct;
  mode basis of T -> Subset-Family of T means
    :Def4:
    for p being Point of T holds it is basis of p;
  existence
  proof
    reconsider F = bool the carrier of T as Subset-Family of T;
    reconsider F as Subset-Family of T;
    take F;
    thus thesis by Th18;
  end;
end;

theorem Th24:
  for T being TopStruct holds bool the carrier of T is basis of T
proof
  let T be TopStruct;
  reconsider P = bool the carrier of T as Subset-Family of T;
  reconsider P as Subset-Family of T;
  P is basis of T
  proof
    let p be Point of T;
    thus thesis by Th18;
  end;
  hence thesis;
end;

theorem Th25:
  for T being non empty TopSpace, P being basis of T holds P is non empty
proof
  let T be non empty TopSpace, P be basis of T;
  set p = the Point of T;
  reconsider C = P as basis of p by Def4;
  C is non empty;
  hence thesis;
end;

registration
  let T be non empty TopSpace;
  cluster -> non empty for basis of T;
  coherence by Th25;
end;

registration
  let T be TopStruct;
  cluster non empty for basis of T;
  existence
  proof
    bool the carrier of T is basis of T by Th24;
    hence thesis;
  end;
end;

theorem
  for T being non empty TopSpace, P being basis of T holds the topology
  of T c= UniCl Int P
proof
  let T be non empty TopSpace, P be basis of T;
  let x be object;
  assume
A1: x in the topology of T;
  then reconsider X = x as Subset of T;
  ex Y being Subset-Family of T st Y c= Int P & X = union Y
  proof
    set Y = {A where A is Subset of T: A in Int P & Int A c= X};
    Y c= bool the carrier of T
    proof
      let y be object;
      assume y in Y;
      then ex A being Subset of T st y = A & A in Int P & Int A c= X;
      hence thesis;
    end;
    then reconsider Y as Subset-Family of T;
    reconsider Y as Subset-Family of T;
    take Y;
    hereby
      let y be object;
      assume y in Y;
      then ex A being Subset of T st y = A & A in Int P & Int A c= X;
      hence y in Int P;
    end;
    hereby
      let y be object;
      assume
A2:   y in X;
      then reconsider p = y as Point of T;
      reconsider C = P as basis of p by Def4;
      X is open by A1;
      then p in Int X by A2,TOPS_1:23;
      then consider W being Subset of T such that
A3:   W in C and
A4:   p in Int W and
A5:   W c= X by Def1;
      Int W c= W by TOPS_1:16;
      then
A6:   Int Int W c= X by A5;
      Int W in Int P by A3,TDLAT_2:def 1;
      then Int W in Y by A6;
      hence y in union Y by A4,TARSKI:def 4;
    end;
    let y be object;
    assume y in union Y;
    then consider K being set such that
A7: y in K and
A8: K in Y by TARSKI:def 4;
    consider A being Subset of T such that
A9: A = K and
A10: A in Int P and
A11: Int A c= X by A8;
    reconsider A as Subset of T;
    ex E being Subset of T st A = Int E & E in P by A10,TDLAT_2:def 1;
    hence thesis by A7,A9,A11;
  end;
  hence thesis by CANTOR_1:def 1;
end;

theorem
  for T being TopSpace, P being Basis of T holds P is basis of T
proof
  let T be TopSpace, P be Basis of T;
A1: P c= the topology of T by TOPS_2:64;
  let p be Point of T, A be Subset of T such that
A2: p in Int A;
  the topology of T c= UniCl P & Int A in the topology of T by CANTOR_1:def 2
,PRE_TOPC:def 2;
  then consider Y being Subset-Family of T such that
A3: Y c= P and
A4: Int A = union Y by CANTOR_1:def 1;
  reconsider Y as Subset-Family of T;
  consider K being set such that
A5: p in K and
A6: K in Y by A2,A4,TARSKI:def 4;
  reconsider K as Subset of T by A6;
  take K;
  thus K in P by A3,A6;
  then K is open by A1;
  hence p in Int K by A5,TOPS_1:23;
A7: Int A c= A by TOPS_1:16;
  K c= union Y by A6,ZFMISC_1:74;
  hence thesis by A4,A7;
end;

definition
  let T be non empty TopSpace-like TopRelStr;
  attr T is topological_semilattice means
  :Def5:
  for f being Function of [:T,T qua TopSpace:], T st f = inf_op T
   holds f is continuous;
end;

registration
  cluster reflexive -> topological_semilattice
    for 1-element TopSpace-like TopRelStr;
  coherence
  proof
    let T be 1-element TopSpace-like TopRelStr;
    assume T is reflexive;
    then reconsider W = T as reflexive 1-element TopSpace-like TopRelStr;
    consider d being Element of W such that
A1: the carrier of W = {d} by TEX_1:def 1;
    let f be Function of [:T,T qua TopSpace:], T such that
A2: f = inf_op T;
    now
      let P1 be Subset of T such that
      P1 is closed;
      per cases by TDLAT_3:19;
      suppose
        P1 = {};
        then f"P1 = {}[:T,T qua TopSpace:];
        hence f"P1 is closed;
      end;
      suppose
A3:     P1 = the carrier of W;
A4:     dom f = the carrier of [:T,T qua TopSpace:] by FUNCT_2:def 1
          .= [:the carrier of T,the carrier of T:] by BORSUK_1:def 2;
A5:     f"P1 = [:{d},{d}:]
        proof
          thus for x being object st x in f"P1 holds x in [:{d},{d}:]
              by A1,A4,
FUNCT_1:def 7;
          let x be object;
A6:       [d,d] in [:the carrier of T,the carrier of T:] by ZFMISC_1:87;
          assume x in [:{d},{d}:];
          then x in {[d,d]} by ZFMISC_1:29;
          then
A7:       x = [d,d] by TARSKI:def 1;
          f.(d,d) = d "/\" d by A2,WAYBEL_2:def 4
            .= d by YELLOW_0:25;
          hence thesis by A3,A4,A7,A6,FUNCT_1:def 7;
        end;
        [#][:T,T qua TopSpace:] = [:{d},{d}:] by A1,BORSUK_1:def 2;
        hence f"P1 is closed by A5;
      end;
    end;
    hence thesis;
  end;
end;

theorem Th28:
  for T being topological_semilattice non empty TopSpace-like
  TopRelStr, x being Element of T holds x"/\" is continuous
proof
  let T be topological_semilattice non empty TopSpace-like TopRelStr, x be
  Element of T;
  let p be Point of T, G be a_neighborhood of x"/\".p;
  set TT = [:T,T qua TopSpace:];
A1: the carrier of TT = [:the carrier of T,the carrier of T:]
       by BORSUK_1:def 2;
  then reconsider xp = [x,p] as Point of TT by YELLOW_3:def 2;
  the carrier of [:T,T:] = [:the carrier of T,the carrier of T:] by
YELLOW_3:def 2;
  then reconsider f = inf_op T as Function of TT, T by A1;
A2: f.xp = f.(x,p) .= x "/\" p by WAYBEL_2:def 4;
  G is a_neighborhood of x"/\"p & f is continuous by Def5,WAYBEL_1:def 18;
  then consider H being a_neighborhood of xp such that
A3: f.:H c= G by A2;
  consider A being Subset-Family of TT such that
A4: Int H = union A and
A5: for e being set st e in A ex X1, Y1 being Subset of T st e = [:X1,Y1
  :] & X1 is open & Y1 is open by BORSUK_1:5;
  xp in Int H by CONNSP_2:def 1;
  then consider Z being set such that
A6: xp in Z and
A7: Z in A by A4,TARSKI:def 4;
  consider X1, Y1 being Subset of T such that
A8: Z = [:X1,Y1:] and
  X1 is open and
A9: Y1 is open by A5,A7;
  p in Y1 by A6,A8,ZFMISC_1:87;
  then reconsider Y1 as a_neighborhood of p by A9,CONNSP_2:3;
  take Y1;
  let b be object;
  assume b in (x"/\").:Y1;
  then consider a being object such that
  a in dom (x"/\") and
A10: a in Y1 and
A11: b = x"/\".a by FUNCT_1:def 6;
  reconsider a as Element of T by A10;
  x in X1 by A6,A8,ZFMISC_1:87;
  then [x,a] in Z by A8,A10,ZFMISC_1:87;
  then
A12: [x,a] in Int H by A4,A7,TARSKI:def 4;
  [x,a] in [:the carrier of T,the carrier of T:] by ZFMISC_1:87;
  then
A13: Int H c= H & [x,a] in dom f by A1,FUNCT_2:def 1,TOPS_1:16;
  b = x "/\" a by A11,WAYBEL_1:def 18
    .= f.(x,a) by WAYBEL_2:def 4;
  then b in f.:H by A12,A13,FUNCT_1:def 6;
  hence thesis by A3;
end;

registration
  let T be topological_semilatticenon empty TopSpace-like TopRelStr, x be
  Element of T;
  cluster x"/\" -> continuous;
  coherence by Th28;
end;