:: YELLOW13 semantic presentation

begin

theorem Th1: :: YELLOW13:1
for T being non empty T_1 TopSpace
for A being finite Subset of T holds A is closed
proof
let T be non empty T_1 TopSpace; ::_thesis: for A being finite Subset of T holds A is closed
let A be finite Subset of T; ::_thesis: A is closed
defpred S1[ set ] means  ex S being Subset of T st
( $1 = S & S is closed );
A1: S1[ {} ]
proof
take  {} T ; ::_thesis: ( {} = {} T & {} T is closed )
thus  {} T = {} ; ::_thesis: {} T is closed
thus  {} T is closed ; ::_thesis: verum
end;
A2: for x, C being set st x in A & C c= A & S1[C] holds
S1[C \/ {x}]
proof
let x, C be set ; ::_thesis: ( x in A & C c= A & S1[C] implies S1[C \/ {x}] )
assume that
A3: x in A and
 C c= A and
A4: S1[C] ; ::_thesis: S1[C \/ {x}]
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  S1[C \/ {x}] by A5; ::_thesis: verum
end;
A7: A is finite ;
 S1[A] from FINSET_1:sch_2(A7, A1, A2);
hence  A is closed ; ::_thesis: verum
end;

registration
let T be non empty T_1 TopSpace;
cluster finite  ->  closed for Element of bool the carrier of T;
coherence
 for b1 being Subset of T st b1 is finite holds
b1 is closed by Th1;
end;

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

registration
cluster non empty finite TopSpace-like T_1  ->  non empty discrete for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is finite & b1 is T_1 holds
b1 is discrete
proof
let T be non empty TopSpace; ::_thesis: ( T is finite & T is T_1 implies T is discrete )
assume  ( T is finite & T is T_1 ) ; ::_thesis: T is discrete
then  for A being Subset of T holds A is closed ;
hence  T is discrete by TDLAT_3:16; ::_thesis: verum
end;
end;

registration
cluster finite TopSpace-like  ->  compact for TopStruct ;
coherence
 for b1 being TopSpace st b1 is finite holds
b1 is compact
proof
let T be TopSpace; ::_thesis: ( T is finite implies T is compact )
assume  T is finite ; ::_thesis: T is compact
then  the carrier of T is finite ;
hence  T is compact by COMPTS_1:18; ::_thesis: verum
end;
end;

theorem Th2: :: YELLOW13:2
for T being non empty discrete TopSpace holds T is normal
proof
let T be non empty discrete TopSpace; ::_thesis: T is normal
let W, V be Subset of T; :: according to COMPTS_1:def_3 ::_thesis: ( W = {} or V = {} or not W is closed or not V is closed or not W misses V or ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & W c= b1 & V c= b2 & b1 misses b2 ) )
assume that
 W <> {} and
 V <> {} and
 W is closed and
 V is closed and
A1: W /\ V = {} ; :: according to XBOOLE_0:def_7 ::_thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & W c= b1 & V c= b2 & b1 misses b2 )
take P = W; ::_thesis: ex b1 being Element of bool the carrier of T st
( P is open & b1 is open & W c= P & V c= b1 & P misses b1 )
take Q = V; ::_thesis: ( P is open & Q is open & W c= P & V c= Q & P misses Q )
thus  ( P is open & Q is open ) by TDLAT_3:15; ::_thesis: ( W c= P & V c= Q & P misses Q )
thus  ( W c= P & V c= Q & P /\ Q = {} ) by A1; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;

theorem Th3: :: YELLOW13:3
for T being non empty discrete TopSpace holds T is regular
proof
let T be non empty discrete TopSpace; ::_thesis: T is regular
let p be Point of T; :: according to COMPTS_1:def_2 ::_thesis: for b1 being Element of bool the carrier of T holds
( b1 = {} or not b1 is closed or not p in b1 ` or ex b2, b3 being Element of bool the carrier of T st
( b2 is open & b3 is open & p in b2 & b1 c= b3 & b2 misses b3 ) )
let P be Subset of T; ::_thesis: ( P = {} or not P is closed or not p in P ` or ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) )
assume that
 P <> {} and
 P is closed and
A1: p in P ` ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 )
take W = {p}; ::_thesis: ex b1 being Element of bool the carrier of T st
( W is open & b1 is open & p in W & P c= b1 & W misses b1 )
take V = P; ::_thesis: ( W is open & V is open & p in W & P c= V & W misses V )
thus  ( W is open & V is open ) by TDLAT_3:15; ::_thesis: ( p in W & P c= V & W misses V )
A2: not p in P by A1, XBOOLE_0:def_5;
 W /\ V c= {}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in W /\ V or a in {} )
assume A3: a in W /\ V ; ::_thesis: a in {}
assume  not a in {} ; ::_thesis: contradiction
 ( a in W & a in V ) by A3, XBOOLE_0:def_4;
hence  contradiction by A2, TARSKI:def_1; ::_thesis: verum
end;
hence  ( p in W & P c= V & W /\ V = {} ) by TARSKI:def_1; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;

theorem Th4: :: YELLOW13:4
for T being non empty discrete TopSpace holds T is T_2
proof
let T be non empty discrete TopSpace; ::_thesis: T is T_2
let p, q be Point of T; :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume A1: not p = q ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
take W = {p}; ::_thesis: ex b1 being Element of bool the carrier of T st
( W is open & b1 is open & p in W & q in b1 & W misses b1 )
take V = {q}; ::_thesis: ( W is open & V is open & p in W & q in V & W misses V )
thus  ( W is open & V is open ) by TDLAT_3:15; ::_thesis: ( p in W & q in V & W misses V )
 W /\ V c= {}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in W /\ V or a in {} )
assume A2: a in W /\ V ; ::_thesis: a in {}
then  a in W by XBOOLE_0:def_4;
then A3: a = p by TARSKI:def_1;
assume  not a in {} ; ::_thesis: contradiction
 a in V by A2, XBOOLE_0:def_4;
hence  contradiction by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
hence  ( p in W & q in V & W /\ V = {} ) by TARSKI:def_1; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;

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

registration
cluster non empty TopSpace-like discrete  ->  T_1 T_2 regular normal for TopStruct ;
coherence
 for b1 being TopSpace st b1 is discrete & not b1 is empty holds
( b1 is normal & b1 is regular & b1 is T_2 & b1 is T_1 ) by Th2, Th3, Th4, Th5;
end;

registration
cluster non empty TopSpace-like T_4  ->  non empty regular for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is T_4 holds
b1 is regular
proof
let T be non empty TopSpace; ::_thesis: ( T is T_4 implies T is regular )
assume A1: T is T_4 ; ::_thesis: T is regular
let p be Point of T; :: according to COMPTS_1:def_2 ::_thesis: for b1 being Element of bool the carrier of T holds
( b1 = {} or not b1 is closed or not p in b1 ` or ex b2, b3 being Element of bool the carrier of T st
( b2 is open & b3 is open & p in b2 & b1 c= b3 & b2 misses b3 ) )
let P be Subset of T; ::_thesis: ( P = {} or not P is closed or not p in P ` or ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) )
assume that
A2: ( P <> {} & P is closed ) and
A3: p in P ` ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 )
A4: not p in P by A3, XBOOLE_0:def_5;
 P /\ {p} c= {}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in P /\ {p} or a in {} )
assume A5: a in P /\ {p} ; ::_thesis: a in {}
assume  not a in {} ; ::_thesis: contradiction
 ( a in P & a in {p} ) by A5, XBOOLE_0:def_4;
hence  contradiction by A4, TARSKI:def_1; ::_thesis: verum
end;
then  P /\ {p} = {} ;
then  P misses {p} by XBOOLE_0:def_7;
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 ; ::_thesis: ex b1 being Element of bool the carrier of T st
( R is open & b1 is open & p in R & P c= b1 & R misses b1 )
take  Q ; ::_thesis: ( R is open & Q is open & p in R & P c= Q & R misses Q )
 p in {p} by TARSKI:def_1;
hence  ( R is open & Q is open & p in R & P c= Q & R misses Q ) by A6; ::_thesis: verum
end;
end;

registration
cluster TopSpace-like T_3  ->  T_2 for TopStruct ;
coherence
 for b1 being TopSpace st b1 is T_3 holds
b1 is T_2
proof
let T be TopSpace; ::_thesis: ( T is T_3 implies T is T_2 )
assume A1: T is T_3 ; ::_thesis: T is T_2
let p, q be Point of T; :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume A2: p <> q ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
then A3: not p in {q} by TARSKI:def_1;
now__::_thesis:_not_the_carrier_of_T_=_{}
assume A4: the carrier of T = {} ; ::_thesis: contradiction
then  p = {} by SUBSET_1:def_1;
hence  contradiction by A2, A4, SUBSET_1:def_1; ::_thesis: verum
end;
then reconsider T9 = T as non empty TopSpace ;
reconsider p = p, q = 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 ; ::_thesis: ex b1 being Element of bool the carrier of T st
( W is open & b1 is open & p in W & q in b1 & W misses b1 )
take  V ; ::_thesis: ( W is open & V is open & p in W & q in V & W misses V )
 q in {q} by TARSKI:def_1;
hence  ( W is open & V is open & p in W & q in V & W misses V ) by A5; ::_thesis: verum
end;
end;

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

theorem :: YELLOW13:7
for S being reflexive RelStr
for T being reflexive transitive RelStr
for f being Function of S,T
for X being Subset of S st f is monotone holds
downarrow (f .: X) = downarrow (f .: (downarrow X))
proof
let S be reflexive RelStr ; ::_thesis: for T being reflexive transitive RelStr
for f being Function of S,T
for X being Subset of S st f is monotone holds
downarrow (f .: X) = downarrow (f .: (downarrow X))
let T be reflexive transitive RelStr ; ::_thesis: for f being Function of S,T
for X being Subset of S st f is monotone holds
downarrow (f .: X) = downarrow (f .: (downarrow X))
let f be Function of S,T; ::_thesis: for X being Subset of S st f is monotone holds
downarrow (f .: X) = downarrow (f .: (downarrow X))
let X be Subset of S; ::_thesis: ( f is monotone implies downarrow (f .: X) = downarrow (f .: (downarrow X)) )
assume A1: f is monotone ; ::_thesis: downarrow (f .: X) = downarrow (f .: (downarrow X))
thus  downarrow (f .: X) c= downarrow (f .: (downarrow X)) by Th6; :: according to XBOOLE_0:def_10 ::_thesis: downarrow (f .: (downarrow X)) c= downarrow (f .: X)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in downarrow (f .: (downarrow X)) or a in downarrow (f .: X) )
assume A2: a in downarrow (f .: (downarrow X)) ; ::_thesis: a in downarrow (f .: 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 set  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 = 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  a in downarrow (f .: X) by A10, WAYBEL_0:def_15; ::_thesis: verum
end;

theorem Th8: :: YELLOW13:8
for N being non empty Poset holds IdsMap N is V13()
proof
let N be non empty Poset; ::_thesis: IdsMap N is V13()
set f = IdsMap N;
let x, y be Element of N; :: according to WAYBEL_1:def_1 ::_thesis: ( not (IdsMap N) . x = (IdsMap N) . y or x = y )
assume A1: (IdsMap N) . x = (IdsMap N) . y ; ::_thesis: x = y
 ( (IdsMap N) . x = downarrow x & (IdsMap N) . y = downarrow y ) by YELLOW_2:def_4;
hence  x = y by A1, WAYBEL_0:19; ::_thesis: verum
end;

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

theorem Th9: :: YELLOW13:9
for N being finite LATTICE holds SupMap N is V13()
proof
let N be finite LATTICE; ::_thesis: SupMap N is V13()
set f = SupMap N;
let x, y be Element of (InclPoset (Ids N)); :: according to WAYBEL_1:def_1 ::_thesis: ( not (SupMap N) . x = (SupMap N) . y or x = y )
assume A1: (SupMap N) . x = (SupMap N) . y ; ::_thesis: x = y
reconsider X = x, Y = y as Ideal of N by YELLOW_2:41;
A2: ( (SupMap N) . x = sup X & (SupMap N) . y = sup Y ) by YELLOW_2:def_3;
 X = Y
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: Y c= X
let a be set ; ::_thesis: ( a in X implies a in Y )
A3: sup Y in Y by WAYBEL_3:16;
assume A4: a in X ; ::_thesis: a in Y
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; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in X )
A5: sup X in X by WAYBEL_3:16;
assume A6: a in Y ; ::_thesis: a in X
then reconsider b = a as Element of N ;
 b <= sup X by A1, A2, A6, YELLOW_0:17, YELLOW_4:1;
hence  a in X by A5, WAYBEL_0:def_19; ::_thesis: verum
end;
hence  x = y ; ::_thesis: verum
end;

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

theorem :: YELLOW13:10
for N being finite LATTICE holds N, InclPoset (Ids N) are_isomorphic
proof
let N be finite LATTICE; ::_thesis: N, InclPoset (Ids N) are_isomorphic
set I = InclPoset (Ids N);
take i = IdsMap N; :: according to WAYBEL_1:def_8 ::_thesis: i is V220(N, InclPoset (Ids N))
 ( not N is empty & not InclPoset (Ids N) is empty implies ( i is V13() & i is monotone & ex s being Function of (InclPoset (Ids N)),N st
( s = i " & s is monotone ) ) )
proof
assume that
 not N is empty and
 not InclPoset (Ids N) is empty ; ::_thesis: ( i is V13() & i is monotone & ex s being Function of (InclPoset (Ids N)),N st
( s = i " & s is monotone ) )
thus  ( i is V13() & i is monotone ) ; ::_thesis: ex s being Function of (InclPoset (Ids N)),N st
( s = i " & s is monotone )
take s = SupMap N; ::_thesis: ( s = i " & s is monotone )
 [i,s] is Galois by WAYBEL_1:57;
then  i is onto by WAYBEL_1:24;
then A1: rng i = the carrier of (InclPoset (Ids N)) by FUNCT_2:def_3;
A2: for y, x being set holds
( y in rng i & x = s . y iff ( x in dom i & y = i . x ) )
proof
let y, x be set ; ::_thesis: ( y in rng i & x = s . y iff ( x in dom i & y = i . x ) )
A3: dom i = the carrier of N by FUNCT_2:def_1;
hereby  ::_thesis: ( x in dom i & y = i . x implies ( y in rng i & x = s . y ) )
assume that
A4: y in rng i and
A5: x = s . y ; ::_thesis: ( x in dom i & i . x = y )
reconsider Y = y as Element of (InclPoset (Ids N)) by A4;
 x = s . Y by A5;
hence  x in dom i by A3; ::_thesis: i . x = y
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 ; ::_thesis: verum
end;
assume that
A6: x in dom i and
A7: y = i . x ; ::_thesis: ( y in rng i & x = s . y )
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; ::_thesis: x = s . y
thus s . y = sup Y by YELLOW_2:def_3
.= sup (downarrow X) by A7, YELLOW_2:def_4
.= x by WAYBEL_0:34 ; ::_thesis: verum
end;
 dom s = the carrier of (InclPoset (Ids N)) by FUNCT_2:def_1;
hence  s = i " by A1, A2, FUNCT_1:32; ::_thesis: s is monotone
thus  s is monotone ; ::_thesis: verum
end;
hence  i is V220(N, InclPoset (Ids N)) by WAYBEL_0:def_38; ::_thesis: verum
end;

theorem Th11: :: YELLOW13:11
for N being non empty complete Poset
for x being Element of N
for X being non empty Subset of N holds x "/\" preserves_inf_of X
proof
let N be non empty complete Poset; ::_thesis: for x being Element of N
for X being non empty Subset of N holds x "/\" preserves_inf_of X
let x be Element of N; ::_thesis: for X being non empty Subset of N holds x "/\" preserves_inf_of X
let X be non empty Subset of N; ::_thesis: x "/\" preserves_inf_of X
assume A1: ex_inf_of X,N ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (x "/\") .: X,N & "/\" (((x "/\") .: X),N) = (x "/\") . ("/\" (X,N)) )
A2: for b being Element of N st b is_<=_than (x "/\") .: X holds
(x "/\") . (inf X) >= b
proof
consider y being set  such that
A3: y in X by XBOOLE_0:def_1;
reconsider y = y as Element of N by A3;
let b be Element of N; ::_thesis: ( b is_<=_than (x "/\") .: X implies (x "/\") . (inf X) >= b )
assume A4: b is_<=_than (x "/\") .: X ; ::_thesis: (x "/\") . (inf X) >= b
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, LATTICE3:def_8;
 X is_>=_than b
proof
let c be Element of N; :: according to LATTICE3:def_8 ::_thesis: ( not c in X or b <= c )
assume  c in X ; ::_thesis: b <= c
then  x "/\" c in (x "/\") .: X by A5;
then A7: b <= x "/\" c by A4, LATTICE3:def_8;
 x "/\" c <= c by YELLOW_0:23;
hence  b <= c by A7, ORDERS_2:3; ::_thesis: verum
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; ::_thesis: verum
end;
thus  ex_inf_of (x "/\") .: X,N by YELLOW_0:17; ::_thesis: "/\" (((x "/\") .: X),N) = (x "/\") . ("/\" (X,N))
 inf X is_<=_than X by A1, YELLOW_0:def_10;
then  (x "/\") . (inf X) is_<=_than (x "/\") .: X by YELLOW_2:13;
hence  "/\" (((x "/\") .: X),N) = (x "/\") . ("/\" (X,N)) by A2, YELLOW_0:33; ::_thesis: verum
end;

theorem Th12: :: YELLOW13:12
for N being non empty complete Poset
for x being Element of N holds x "/\" is meet-preserving
proof
let N be non empty complete Poset; ::_thesis: for x being Element of N holds x "/\" is meet-preserving
let x be Element of N; ::_thesis: x "/\" is meet-preserving
let a, b be Element of N; :: according to WAYBEL_0:def_34 ::_thesis: x "/\" preserves_inf_of {a,b}
thus  x "/\" preserves_inf_of {a,b} by Th11; ::_thesis: verum
end;

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

begin

theorem :: YELLOW13:13
for T being non empty anti-discrete TopStruct
for p being Point of T holds { the carrier of T} is Basis of
proof
let T be non empty anti-discrete TopStruct ; ::_thesis: for p being Point of T holds { the carrier of T} is Basis of
let p be Point of T; ::_thesis: { the carrier of T} is Basis of
set A = { the carrier of T};
 { the carrier of T} c= bool the carrier of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { the carrier of T} or a in bool the carrier of T )
assume  a in { the carrier of T} ; ::_thesis: a in bool the carrier of T
then A1: a = the carrier of T by TARSKI:def_1;
 the carrier of T c= the carrier of T ;
hence  a in bool the carrier of T by A1; ::_thesis: verum
end;
then reconsider A = { the carrier of T} as Subset-Family of T ;
 A is Basis of
proof
A2: A is open
proof
let a be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not a in A or a is open )
assume  a in A ; ::_thesis: a is open
then  a = [#] T by TARSKI:def_1;
hence  a is open ; ::_thesis: verum
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 ; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of T holds
( not b1 is open or not p in b1 or ex b2 being Element of bool the carrier of T st
( b2 in A & b2 c= b1 ) )
let S be Subset of T; ::_thesis: ( not S is open or not p in S or ex b1 being Element of bool the carrier of T st
( b1 in A & b1 c= S ) )
assume  ( S is open & p in S ) ; ::_thesis: ex b1 being Element of bool the carrier of T st
( b1 in A & b1 c= S )
then A3: S = the carrier of T by TDLAT_3:18;
take  S ; ::_thesis: ( S in A & S c= S )
thus  ( S in A & S c= S ) by A3, TARSKI:def_1; ::_thesis: verum
end;
hence  A is Basis of by A2; ::_thesis: verum
end;
hence  { the carrier of T} is Basis of ; ::_thesis: verum
end;

theorem :: YELLOW13:14
for T being non empty anti-discrete TopStruct
for p being Point of T
for D being Basis of holds D = { the carrier of T}
proof
let T be non empty anti-discrete TopStruct ; ::_thesis: for p being Point of T
for D being Basis of holds D = { the carrier of T}
let p be Point of T; ::_thesis: for D being Basis of holds D = { the carrier of T}
let D be Basis of ; ::_thesis: D = { the carrier of T}
thus  D c= { the carrier of T} :: according to XBOOLE_0:def_10 ::_thesis: { the carrier of T} c= D
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in D or a in { the carrier of T} )
assume A1: a in D ; ::_thesis: a in { the carrier of T}
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  a in { the carrier of T} by TARSKI:def_1; ::_thesis: verum
end;
hence  { the carrier of T} c= D by ZFMISC_1:33; ::_thesis: verum
end;

theorem :: YELLOW13:15
for T being non empty TopSpace
for P being Basis of T
for p being Point of T holds  {  A where A is Subset of T : ( A in P & p in A )  }  is Basis of
proof
let T be non empty TopSpace; ::_thesis: for P being Basis of T
for p being Point of T holds  {  A where A is Subset of T : ( A in P & p in A )  }  is Basis of
let P be Basis of T; ::_thesis: for p being Point of T holds  {  A where A is Subset of T : ( A in P & p in A )  }  is Basis of
let p be Point of T; ::_thesis:  {  A where A is Subset of T : ( A in P & p in A )  }  is Basis of
set Z =  {  A where A is Subset of T : ( A in P & p in A )  }  ;
  {  A where A is Subset of T : ( A in P & p in A )  }  c= bool the carrier of T
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  A where A is Subset of T : ( A in P & p in A )  }  or z in bool the carrier of T )
assume  z in  {  A where A is Subset of T : ( A in P & p in A )  }  ; ::_thesis: z in bool the carrier of T
then  ex A being Subset of T st
( A = z & A in P & p in A ) ;
hence  z in bool the carrier of T ; ::_thesis: verum
end;
then reconsider Z =  {  A where A is Subset of T : ( A in P & p in A )  }  as Subset-Family of T ;
reconsider Z = Z as Subset-Family of T ;
 Z is Basis of
proof
A1: Z is open
proof
let z be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not z in Z or z is open )
assume  z in Z ; ::_thesis: z is open
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  z is open by A2; ::_thesis: verum
end;
 Z is p -quasi_basis
proof
now__::_thesis:_for_z_being_set_st_z_in_Z_holds_
p_in_z
let z be set ; ::_thesis: ( z in Z implies p in z )
assume  z in Z ; ::_thesis: p in z
then  ex A being Subset of T st
( A = z & A in P & p in A ) ;
hence  p in z ; ::_thesis: verum
end;
hence  p in Intersect Z by SETFAM_1:43; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of T holds
( not b1 is open or not p in b1 or ex b2 being Element of bool the carrier of T st
( b2 in Z & b2 c= b1 ) )
let S be Subset of T; ::_thesis: ( not S is open or not p in S or ex b1 being Element of bool the carrier of T st
( b1 in Z & b1 c= S ) )
assume  ( S is open & p in S ) ; ::_thesis: ex b1 being Element of bool the carrier of T st
( b1 in Z & b1 c= 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 ; ::_thesis: ( V in Z & V c= S )
thus  ( V in Z & V c= S ) by A4; ::_thesis: verum
end;
hence  Z is Basis of by A1; ::_thesis: verum
end;
hence   {  A where A is Subset of T : ( A in P & p in A )  }  is Basis of ; ::_thesis: verum
end;

Lm1:  for T being non empty TopStruct
for A being Subset of T
for p being Point of T st p in Cl A holds
for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q
proof
let T be non empty TopStruct ; ::_thesis: for A being Subset of T
for p being Point of T st p in Cl A holds
for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q
let A be Subset of T; ::_thesis: for p being Point of T st p in Cl A holds
for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q
let p be Point of T; ::_thesis: ( p in Cl A implies for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q )
assume A1: p in Cl A ; ::_thesis: for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q
let K be Basis of ; ::_thesis: for Q being Subset of T st Q in K holds
A meets Q
let Q be Subset of T; ::_thesis: ( Q in K implies A meets Q )
assume  Q in K ; ::_thesis: A meets Q
then  ( Q is open & p in Q ) by YELLOW_8:12;
then  A meets Q by A1, PRE_TOPC:def_7;
hence  A /\ Q <> {} by XBOOLE_0:def_7; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;

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

Lm3:  for T being non empty TopStruct
for A being Subset of T
for p being Point of T st ex K being Basis of 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 ; ::_thesis: for A being Subset of T
for p being Point of T st ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q holds
p in Cl A
let A be Subset of T; ::_thesis: for p being Point of T st ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q holds
p in Cl A
let p be Point of T; ::_thesis: ( ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q implies p in Cl A )
given K being Basis of  such that A1: for Q being Subset of T st Q in K holds
A meets Q ; ::_thesis: p in Cl A
assume  not p in Cl A ; ::_thesis: contradiction
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, TOPS_1:3, 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; ::_thesis: verum
end;

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

theorem :: YELLOW13:17
for T being non empty TopStruct
for A being Subset of T
for p being Point of T holds
( p in Cl A iff ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q )
proof
let T be non empty TopStruct ; ::_thesis: for A being Subset of T
for p being Point of T holds
( p in Cl A iff ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q )
let A be Subset of T; ::_thesis: for p being Point of T holds
( p in Cl A iff ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q )
let p be Point of T; ::_thesis: ( p in Cl A iff ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q )
hereby  ::_thesis: ( ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q implies p in Cl A )
assume  p in Cl A ; ::_thesis: ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q
then  for K being Basis of
for Q being Subset of T st Q in K holds
A meets Q by Lm1;
hence  ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q by Lm2; ::_thesis: verum
end;
assume  ex K being Basis of st
for Q being Subset of T st Q in K holds
A meets Q ; ::_thesis: p in Cl A
hence  p in Cl A by Lm3; ::_thesis: verum
end;

definition
let T be TopStruct ;
let p be Point of T;
mode basis of p ->  Subset-Family of T means :Def1: :: YELLOW13:def 1
 for A being Subset of T st p in Int A holds
ex P being Subset of T st
( P in it & p in Int P & P c= A );
existence
 ex b1 being Subset-Family of T st
for A being Subset of T st p in Int A holds
ex P being Subset of T st
( P in b1 & p in Int P & P c= A )
proof
reconsider F = bool the carrier of T as Subset-Family of T ;
reconsider F = F as Subset-Family of T ;
take  F ; ::_thesis: for A being Subset of T st p in Int A holds
ex P being Subset of T st
( P in F & p in Int P & P c= A )
let A be Subset of T; ::_thesis: ( p in Int A implies ex P being Subset of T st
( P in F & p in Int P & P c= A ) )
assume A1: p in Int A ; ::_thesis: ex P being Subset of T st
( P in F & p in Int P & P c= A )
take  Int A ; ::_thesis: ( Int A in F & p in Int (Int A) & Int A c= A )
thus  ( Int A in F & p in Int (Int A) & Int A c= A ) by A1, TOPS_1:16; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines basis YELLOW13:def_1_:_
 for T being TopStruct
for p being Point of T
for b3 being Subset-Family of T holds
( b3 is basis of p iff for A being Subset of T st p in Int A holds
ex P being Subset of T st
( P in b3 & p in Int P & P c= A ) );

definition
let T be non empty TopSpace;
let p be Point of T;
redefine mode basis of p means :: YELLOW13:def 2
 for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in it & P c= A );
compatibility
 for b1 being Subset-Family of T holds
( b1 is basis of p iff for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in b1 & P c= A ) )
proof
let F be Subset-Family of T; ::_thesis: ( F is basis of p iff for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in F & P c= A ) )
hereby  ::_thesis: ( ( for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in F & P c= A ) ) implies F is basis of p )
assume A1: F is basis of p ; ::_thesis: for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in F & P c= A )
let A be a_neighborhood of p; ::_thesis: ex P being a_neighborhood of p st
( P in F & P c= A )
 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 = P as a_neighborhood of p by A3, CONNSP_2:def_1;
take P = P; ::_thesis: ( P in F & P c= A )
thus  ( P in F & P c= A ) by A2, A4; ::_thesis: verum
end;
assume A5: for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in F & P c= A ) ; ::_thesis: F is basis of p
let A be Subset of T; :: according to YELLOW13:def_1 ::_thesis: ( p in Int A implies ex P being Subset of T st
( P in F & p in Int P & P c= A ) )
assume  p in Int A ; ::_thesis: ex P being Subset of T st
( P in F & p in Int P & P c= 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 ; ::_thesis: ( P in F & p in Int P & P c= A )
thus  ( P in F & p in Int P & P c= A ) by A6, CONNSP_2:def_1; ::_thesis: verum
end;
end;

:: deftheorem  defines basis YELLOW13:def_2_:_
 for T being non empty TopSpace
for p being Point of T
for b3 being Subset-Family of T holds
( b3 is basis of p iff for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in b3 & P c= A ) );

theorem Th18: :: YELLOW13:18
for T being TopStruct
for p being Point of T holds bool the carrier of T is basis of p
proof
let T be TopStruct ; ::_thesis: for p being Point of T holds bool the carrier of T is basis of p
let p be Point of T; ::_thesis: bool the carrier of T is basis of p
reconsider F = bool the carrier of T as Subset-Family of T ;
reconsider F = F as Subset-Family of T ;
 F is basis of p
proof
let A be Subset of T; :: according to YELLOW13:def_1 ::_thesis: ( p in Int A implies ex P being Subset of T st
( P in F & p in Int P & P c= A ) )
assume A1: p in Int A ; ::_thesis: ex P being Subset of T st
( P in F & p in Int P & P c= A )
take  Int A ; ::_thesis: ( Int A in F & p in Int (Int A) & Int A c= A )
thus  ( Int A in F & p in Int (Int A) & Int A c= A ) by A1, TOPS_1:16; ::_thesis: verum
end;
hence  bool the carrier of T is basis of p ; ::_thesis: verum
end;

theorem Th19: :: YELLOW13:19
for T being non empty TopSpace
for p being Point of T
for P being basis of p holds not P is empty
proof
let T be non empty TopSpace; ::_thesis: for p being Point of T
for P being basis of p holds not P is empty
let p be Point of T; ::_thesis: for P being basis of p holds not P is empty
let P be basis of p; ::_thesis: not P is empty
 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  not P is empty ; ::_thesis: verum
end;

registration
let T be non empty TopSpace;
let p be Point of T;
cluster  ->  non empty for basis of p;
coherence
 for b1 being basis of p holds not b1 is empty by Th19;
end;

registration
let T be TopStruct ;
let p be Point of T;
cluster non empty for basis of p;
existence
 not for b1 being basis of p holds b1 is empty
proof
 bool the carrier of T is basis of p by Th18;
hence  not for b1 being basis of p holds b1 is empty ; ::_thesis: verum
end;
end;

definition
let T be TopStruct ;
let p be Point of T;
let P be basis of p;
attrP is correct  means :Def3: :: YELLOW13:def 3
 for A being Subset of T holds
( A in P iff p in Int A );
end;

:: deftheorem Def3 defines correct YELLOW13:def_3_:_
 for T being TopStruct
for p being Point of T
for P being basis of p holds
( P is correct iff for A being Subset of T holds
( A in P iff p in Int A ) );

Lm4: now__::_thesis:_for_T_being_TopStruct_
for_p_being_Point_of_T
for_K_being_set_st_K_=__{__A_where_A_is_Subset_of_T_:_p_in_Int_A__}__holds_
K_is_basis_of_p
let T be TopStruct ; ::_thesis: for p being Point of T
for K being set st K =  {  A where A is Subset of T : p in Int A  }  holds
K is basis of p
let p be Point of T; ::_thesis: for K being set st K =  {  A where A is Subset of T : p in Int A  }  holds
K is basis of p
let K be set ; ::_thesis: ( K =  {  A where A is Subset of T : p in Int A  }  implies K is basis of p )
assume A1: K =  {  A where A is Subset of T : p in Int A  }  ; ::_thesis: K is basis of p
 K c= bool the carrier of T
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in K or y in bool the carrier of T )
assume  y in K ; ::_thesis: y in bool the carrier of T
then  ex A being Subset of T st
( y = A & p in Int A ) by A1;
hence  y in bool the carrier of T ; ::_thesis: verum
end;
then reconsider J = K as Subset-Family of T ;
reconsider J = J as Subset-Family of T ;
 for A being Subset of T st p in Int A holds
ex P being Subset of T st
( P in J & p in Int P & P c= A )
proof
let A be Subset of T; ::_thesis: ( p in Int A implies ex P being Subset of T st
( P in J & p in Int P & P c= A ) )
assume A2: p in Int A ; ::_thesis: ex P being Subset of T st
( P in J & p in Int P & P c= A )
take P = A; ::_thesis: ( P in J & p in Int P & P c= A )
thus  ( P in J & p in Int P & P c= A ) by A1, A2; ::_thesis: verum
end;
hence  K is basis of p by Def1; ::_thesis: verum
end;

Lm5: now__::_thesis:_for_T_being_TopStruct_
for_p_being_Point_of_T
for_K_being_basis_of_p_st_K_=__{__A_where_A_is_Subset_of_T_:_p_in_Int_A__}__holds_
K_is_correct
let T be TopStruct ; ::_thesis: for p being Point of T
for K being basis of p st K =  {  A where A is Subset of T : p in Int A  }  holds
K is correct
let p be Point of T; ::_thesis: for K being basis of p st K =  {  A where A is Subset of T : p in Int A  }  holds
K is correct
let K be basis of p; ::_thesis: ( K =  {  A where A is Subset of T : p in Int A  }  implies K is correct )
assume A1: K =  {  A where A is Subset of T : p in Int A  }  ; ::_thesis: K is correct
thus  K is correct ::_thesis: verum
proof
let A be Subset of T; :: according to YELLOW13:def_3 ::_thesis: ( A in K iff p in Int A )
hereby  ::_thesis: ( p in Int A implies A in K )
assume  A in K ; ::_thesis: p in Int A
then  ex M being Subset of T st
( A = M & p in Int M ) by A1;
hence  p in Int A ; ::_thesis: verum
end;
thus  ( p in Int A implies A in K ) by A1; ::_thesis: verum
end;
end;

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

theorem :: YELLOW13:20
for T being TopStruct
for 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;
let p be Point of T;
cluster non empty correct for basis of p;
existence
 ex b1 being basis of p st
( not b1 is empty & b1 is correct )
proof
reconsider K =  {  A where A is Subset of T : p in Int A  }  as correct basis of p by Lm4, Lm5;
take  K ; ::_thesis: ( not K is empty & K is correct )
thus  ( not K is empty & K is correct ) ; ::_thesis: verum
end;
end;

theorem :: YELLOW13:21
for T being non empty anti-discrete TopStruct
for p being Point of T holds { the carrier of T} is correct basis of p
proof
let T be non empty anti-discrete TopStruct ; ::_thesis: for p being Point of T holds { the carrier of T} is correct basis of p
let p be Point of T; ::_thesis: { the carrier of T} is correct basis of p
set A = { the carrier of T};
 { the carrier of T} c= bool the carrier of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { the carrier of T} or a in bool the carrier of T )
assume  a in { the carrier of T} ; ::_thesis: a in bool the carrier of T
then A1: a = the carrier of T by TARSKI:def_1;
 the carrier of T c= the carrier of T ;
hence  a in bool the carrier of T by A1; ::_thesis: verum
end;
then reconsider A = { the carrier of T} as Subset-Family of T ;
reconsider A = A as Subset-Family of T ;
 A is basis of p
proof
let S be a_neighborhood of p; :: according to YELLOW13:def_2 ::_thesis: ex P being a_neighborhood of p st
( P in A & P c= S )
take  S ; ::_thesis: ( S in A & S c= 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, XBOOLE_0:def_10;
hence  ( S in A & S c= S ) by A2, TARSKI:def_1; ::_thesis: verum
end;
then reconsider A = A as basis of p ;
 A is correct
proof
let X be Subset of T; :: according to YELLOW13:def_3 ::_thesis: ( X in A iff p in Int X )
hereby  ::_thesis: ( p in Int X implies X in A )
assume  X in A ; ::_thesis: p in Int X
then  X = the carrier of T by TARSKI:def_1;
then  Int X = [#] T by TOPS_1:15;
hence  p in Int X ; ::_thesis: verum
end;
assume  p in Int X ; ::_thesis: X in A
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, XBOOLE_0:def_10;
hence  X in A by A3, TARSKI:def_1; ::_thesis: verum
end;
hence  { the carrier of T} is correct basis of p ; ::_thesis: verum
end;

theorem :: YELLOW13:22
for T being non empty anti-discrete TopStruct
for p being Point of T
for D being correct basis of p holds D = { the carrier of T}
proof
let T be non empty anti-discrete TopStruct ; ::_thesis: for p being Point of T
for D being correct basis of p holds D = { the carrier of T}
let p be Point of T; ::_thesis: for D being correct basis of p holds D = { the carrier of T}
let D be correct basis of p; ::_thesis: D = { the carrier of T}
thus  D c= { the carrier of T} :: according to XBOOLE_0:def_10 ::_thesis: { the carrier of T} c= D
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in D or a in { the carrier of T} )
assume A1: a in D ; ::_thesis: a in { the carrier of T}
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, XBOOLE_0:def_10;
hence  a in { the carrier of T} by A2, TARSKI:def_1; ::_thesis: verum
end;
hence  { the carrier of T} c= D by ZFMISC_1:33; ::_thesis: verum
end;

theorem :: YELLOW13:23
for T being non empty TopSpace
for p being Point of T
for P being Basis of holds P is basis of p
proof
let T be non empty TopSpace; ::_thesis: for p being Point of T
for P being Basis of holds P is basis of p
let p be Point of T; ::_thesis: for P being Basis of holds P is basis of p
let P be Basis of ; ::_thesis: P is basis of p
now__::_thesis:_for_A_being_Subset_of_T_st_p_in_Int_A_holds_
ex_V_being_Subset_of_T_st_
(_V_in_P_&_p_in_Int_V_&_V_c=_A_)
let A be Subset of T; ::_thesis: ( p in Int A implies ex V being Subset of T st
( V in P & p in Int V & V c= A ) )
assume  p in Int A ; ::_thesis: ex V being Subset of T st
( V in P & p in Int V & V c= 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; ::_thesis: ( V in P & p in Int V & V c= A )
 V is open by A1, YELLOW_8:12;
then  ( Int A c= A & Int V = V ) by TOPS_1:16, TOPS_1:23;
hence  ( V in P & p in Int V & V c= A ) by A1, A2, XBOOLE_1:1, YELLOW_8:12; ::_thesis: verum
end;
hence  P is basis of p by Def1; ::_thesis: verum
end;

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

:: deftheorem Def4 defines basis YELLOW13:def_4_:_
 for T being TopStruct
for b2 being Subset-Family of T holds
( b2 is basis of T iff for p being Point of T holds b2 is basis of p );

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

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

registration
let T be non empty TopSpace;
cluster  ->  non empty for basis of T;
coherence
 for b1 being basis of T holds not b1 is empty by Th25;
end;

registration
let T be TopStruct ;
cluster non empty for basis of T;
existence
 not for b1 being basis of T holds b1 is empty
proof
 bool the carrier of T is basis of T by Th24;
hence  not for b1 being basis of T holds b1 is empty ; ::_thesis: verum
end;
end;

theorem :: YELLOW13:26
for T being non empty TopSpace
for P being basis of T holds the topology of T c= UniCl (Int P)
proof
let T be non empty TopSpace; ::_thesis: for P being basis of T holds the topology of T c= UniCl (Int P)
let P be basis of T; ::_thesis: the topology of T c= UniCl (Int P)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of T or x in UniCl (Int P) )
assume A1: x in the topology of T ; ::_thesis: x in UniCl (Int P)
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 )  }  ;
  {  A where A is Subset of T : ( A in Int P & Int A c= x )  }  c= bool the carrier of T
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  A where A is Subset of T : ( A in Int P & Int A c= x )  }  or y in bool the carrier of T )
assume  y in  {  A where A is Subset of T : ( A in Int P & Int A c= x )  }  ; ::_thesis: y in bool the carrier of T
then  ex A being Subset of T st
( y = A & A in Int P & Int A c= x ) ;
hence  y in bool the carrier of T ; ::_thesis: verum
end;
then reconsider Y =  {  A where A is Subset of T : ( A in Int P & Int A c= x )  }  as Subset-Family of T ;
reconsider Y = Y as Subset-Family of T ;
take  Y ; ::_thesis: ( Y c= Int P & X = union Y )
hereby  :: according to TARSKI:def_3 ::_thesis: X = union Y
let y be set ; ::_thesis: ( y in Y implies y in Int P )
assume  y in Y ; ::_thesis: y in Int P
then  ex A being Subset of T st
( y = A & A in Int P & Int A c= x ) ;
hence  y in Int P ; ::_thesis: verum
end;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: union Y c= X
let y be set ; ::_thesis: ( y in X implies y in union Y )
assume A2: y in X ; ::_thesis: y in union Y
then reconsider p = y as Point of T ;
reconsider C = P as basis of p by Def4;
 X is open by A1, PRE_TOPC:def_2;
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, XBOOLE_1:1;
 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; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in union Y or y in X )
assume  y in union Y ; ::_thesis: y in X
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 = 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  y in X by A7, A9, A11; ::_thesis: verum
end;
hence  x in UniCl (Int P) by CANTOR_1:def_1; ::_thesis: verum
end;

theorem :: YELLOW13:27
for T being TopSpace
for P being Basis of T holds P is basis of T
proof
let T be TopSpace; ::_thesis: for P being Basis of T holds P is basis of T
let P be Basis of T; ::_thesis: P is basis of T
A1: P c= the topology of T by TOPS_2:64;
let p be Point of T; :: according to YELLOW13:def_4 ::_thesis: P is basis of p
let A be Subset of T; :: according to YELLOW13:def_1 ::_thesis: ( p in Int A implies ex P being Subset of T st
( P in P & p in Int P & P c= A ) )
assume A2: p in Int A ; ::_thesis: ex P being Subset of T st
( P in P & p in Int P & P c= 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 = 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 = K as Subset of T by A6;
take  K ; ::_thesis: ( K in P & p in Int K & K c= A )
thus  K in P by A3, A6; ::_thesis: ( p in Int K & K c= A )
then  K is open by A1, PRE_TOPC:def_2;
hence  p in Int K by A5, TOPS_1:23; ::_thesis: K c= A
A7: Int A c= A by TOPS_1:16;
 K c= union Y by A6, ZFMISC_1:74;
hence  K c= A by A4, A7, XBOOLE_1:1; ::_thesis: verum
end;

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

:: deftheorem Def5 defines topological_semilattice YELLOW13:def_5_:_
 for T being non empty TopSpace-like TopRelStr holds
( T is topological_semilattice iff for f being Function of [:T,T:],T st f = inf_op T holds
f is continuous );

registration
cluster1 -element TopSpace-like reflexive  -> 1 -element TopSpace-like topological_semilattice for TopRelStr ;
coherence
 for b1 being 1 -element TopSpace-like TopRelStr st b1 is reflexive holds
b1 is topological_semilattice
proof
let T be 1 -element TopSpace-like TopRelStr ; ::_thesis: ( T is reflexive implies T is topological_semilattice )
assume  T is reflexive ; ::_thesis: T is topological_semilattice
then reconsider W = T as 1 -element TopSpace-like reflexive 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:],T; :: according to YELLOW13:def_5 ::_thesis: ( f = inf_op T implies f is continuous )
assume A2: f = inf_op T ; ::_thesis: f is continuous
now__::_thesis:_for_P1_being_Subset_of_T_st_P1_is_closed_holds_
f_"_P1_is_closed
let P1 be Subset of T; ::_thesis: ( P1 is closed implies f " b1 is closed )
assume  P1 is closed ; ::_thesis: f " b1 is closed
percases ( P1 = {} or P1 = the carrier of W ) by TDLAT_3:19;
suppose P1 = {} ; ::_thesis: f " b1 is closed
then  f " P1 = {} [:T,T:] ;
hence  f " P1 is closed ; ::_thesis: verum
end;
supposeA3: P1 = the carrier of W ; ::_thesis: f " b1 is closed
A4: dom f = the carrier of [:T,T:] 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 set st x in f " P1 holds
x in [:{d},{d}:] by A1, A4, FUNCT_1:def_7; :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: [:{d},{d}:] c= f " P1
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:{d},{d}:] or x in f " P1 )
A6: [d,d] in [: the carrier of T, the carrier of T:] by ZFMISC_1:87;
assume  x in [:{d},{d}:] ; ::_thesis: x in f " P1
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  x in f " P1 by A3, A4, A7, A6, FUNCT_1:def_7; ::_thesis: verum
end;
 [#] [:T,T:] = [:{d},{d}:] by A1, BORSUK_1:def_2;
hence  f " P1 is closed by A5; ::_thesis: verum
end;
end;
end;
hence  f is continuous by PRE_TOPC:def_6; ::_thesis: verum
end;
end;

theorem Th28: :: YELLOW13:28
for T being non empty TopSpace-like topological_semilattice TopRelStr
for x being Element of T holds x "/\" is continuous
proof
let T be non empty TopSpace-like topological_semilattice TopRelStr ; ::_thesis: for x being Element of T holds x "/\" is continuous
let x be Element of T; ::_thesis: x "/\" is continuous
let p be Point of T; :: according to BORSUK_1:def_1 ::_thesis: for b1 being a_neighborhood of (x "/\") . p ex b2 being a_neighborhood of p st (x "/\") .: b2 c= b1
let G be a_neighborhood of (x "/\") . p; ::_thesis: ex b1 being a_neighborhood of p st (x "/\") .: b1 c= G
set TT = [:T,T:];
A1: the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def_2;
then reconsider xp = [x,p] as Point of [:T,T:] 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 [:T,T:],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, BORSUK_1:def_1;
consider A being Subset-Family of [:T,T:] such that
A4: Int H = union A and
A5: for e being set st e in A holds
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 = Y1 as a_neighborhood of p by A9, CONNSP_2:3;
take  Y1 ; ::_thesis: (x "/\") .: Y1 c= G
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in (x "/\") .: Y1 or b in G )
assume  b in (x "/\") .: Y1 ; ::_thesis: b in G
then consider a being set  such that
 a in dom (x "/\") and
A10: a in Y1 and
A11: b = (x "/\") . a by FUNCT_1:def_6;
reconsider a = 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  b in G by A3; ::_thesis: verum
end;

registration
let T be non empty TopSpace-like topological_semilattice TopRelStr ;
let x be Element of T;
clusterx "/\"  ->  continuous ;
coherence
 x "/\" is continuous by Th28;
end;