:: YELLOW_9 semantic presentation

begin

scheme :: YELLOW_9:sch 1
FraenkelInvolution{ F1() ->  non empty set , F2() ->  Subset of F1(), F3() ->  Subset of F1(), F4( set ) ->  Element of F1() } :
 F2() =  {  F4(a) where a is Element of F1() : a in F3()  }
provided
A1: F3() =  {  F4(a) where a is Element of F1() : a in F2()  }  and
A2: for a being Element of F1() holds F4(F4(a)) = a
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  F4(a) where a is Element of F1() : a in F3()  }  c= F2()
let x be set ; ::_thesis: ( x in F2() implies x in  {  F4(b) where b is Element of F1() : b in F3()  }  )
assume A3: x in F2() ; ::_thesis: x in  {  F4(b) where b is Element of F1() : b in F3()  }
then reconsider a = x as Element of F1() ;
A4: F4(a) in F3() by A1, A3;
 F4(F4(a)) = a by A2;
hence  x in  {  F4(b) where b is Element of F1() : b in F3()  }  by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F4(a) where a is Element of F1() : a in F3()  }  or x in F2() )
assume  x in  {  F4(b) where b is Element of F1() : b in F3()  }  ; ::_thesis: x in F2()
then consider b being Element of F1() such that
A5: x = F4(b) and
A6: b in F3() ;
 ex a being Element of F1() st
( b = F4(a) & a in F2() ) by A1, A6;
hence  x in F2() by A2, A5; ::_thesis: verum
end;

scheme :: YELLOW_9:sch 2
FraenkelComplement1{ F1() ->  non empty RelStr , F2() ->  Subset-Family of F1(), F3() ->  set , F4( set ) ->  Subset of F1() } :
 COMPLEMENT F2() =  {  (F4(a) `) where a is Element of F1() : a in F3()  }
provided
A1: F2() =  {  F4(a) where a is Element of F1() : a in F3()  }
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  (F4(a) `) where a is Element of F1() : a in F3()  }  c= COMPLEMENT F2()
let x be set ; ::_thesis: ( x in COMPLEMENT F2() implies x in  {  (F4(a) `) where a is Element of F1() : a in F3()  }  )
assume A2: x in COMPLEMENT F2() ; ::_thesis: x in  {  (F4(a) `) where a is Element of F1() : a in F3()  }
then reconsider y = x as Subset of F1() ;
 y ` in F2() by A2, SETFAM_1:def_7;
then A3: ex b being Element of F1() st
( y ` = F4(b) & b in F3() ) by A1;
 x = (y `) ` ;
hence  x in  {  (F4(a) `) where a is Element of F1() : a in F3()  }  by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (F4(a) `) where a is Element of F1() : a in F3()  }  or x in COMPLEMENT F2() )
assume  x in  {  (F4(a) `) where a is Element of F1() : a in F3()  }  ; ::_thesis: x in COMPLEMENT F2()
then consider a being Element of F1() such that
A4: x = F4(a) ` and
A5: a in F3() ;
 F4(a) in F2() by A1, A5;
hence  x in COMPLEMENT F2() by A4, YELLOW_8:5; ::_thesis: verum
end;

scheme :: YELLOW_9:sch 3
FraenkelComplement2{ F1() ->  non empty RelStr , F2() ->  Subset-Family of F1(), F3() ->  set , F4( set ) ->  Subset of F1() } :
 COMPLEMENT F2() =  {  F4(a) where a is Element of F1() : a in F3()  }
provided
A1: F2() =  {  (F4(a) `) where a is Element of F1() : a in F3()  }
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  F4(a) where a is Element of F1() : a in F3()  }  c= COMPLEMENT F2()
let x be set ; ::_thesis: ( x in COMPLEMENT F2() implies x in  {  F4(a) where a is Element of F1() : a in F3()  }  )
assume A2: x in COMPLEMENT F2() ; ::_thesis: x in  {  F4(a) where a is Element of F1() : a in F3()  }
then reconsider y = x as Subset of F1() ;
 y ` in F2() by A2, SETFAM_1:def_7;
then A3: ex b being Element of F1() st
( y ` = F4(b) ` & b in F3() ) by A1;
 x = (y `) ` ;
hence  x in  {  F4(a) where a is Element of F1() : a in F3()  }  by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F4(a) where a is Element of F1() : a in F3()  }  or x in COMPLEMENT F2() )
assume  x in  {  F4(a) where a is Element of F1() : a in F3()  }  ; ::_thesis: x in COMPLEMENT F2()
then consider a being Element of F1() such that
A4: x = F4(a) and
A5: a in F3() ;
 F4(a) ` in F2() by A1, A5;
hence  x in COMPLEMENT F2() by A4, SETFAM_1:def_7; ::_thesis: verum
end;

theorem :: YELLOW_9:1
for R being non empty RelStr
for x, y being Element of R holds
( y in (uparrow x) ` iff not x <= y )
proof
let R be non empty RelStr ; ::_thesis: for x, y being Element of R holds
( y in (uparrow x) ` iff not x <= y )
let x, y be Element of R; ::_thesis: ( y in (uparrow x) ` iff not x <= y )
 (uparrow x) ` = the carrier of R \ (uparrow x) by SUBSET_1:def_4;
then  ( y in (uparrow x) ` iff not y in uparrow x ) by XBOOLE_0:def_5;
hence  ( y in (uparrow x) ` iff not x <= y ) by WAYBEL_0:18; ::_thesis: verum
end;

scheme :: YELLOW_9:sch 4
ABC{ F1() ->  TopSpace, F2( set ) ->  set , F3() ->  Function, P1[ set ] } :
 F3() " (union  {  F2(x) where x is Subset of F1() : P1[x]  }  ) = union  {  (F3() " F2(y)) where y is Subset of F1() : P1[y]  }
proof
set X =  {  F2(x) where x is Subset of F1() : P1[x]  }  ;
set Y =  {  (F3() " F2(y)) where y is Subset of F1() : P1[y]  }  ;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: union  {  (F3() " F2(y)) where y is Subset of F1() : P1[y]  }  c= F3() " (union  {  F2(x) where x is Subset of F1() : P1[x]  }  )
let x be set ; ::_thesis: ( x in F3() " (union  {  F2(x) where x is Subset of F1() : P1[x]  }  ) implies x in union  {  (F3() " F2(y)) where y is Subset of F1() : P1[y]  }  )
assume A1: x in F3() " (union  {  F2(x) where x is Subset of F1() : P1[x]  }  ) ; ::_thesis: x in union  {  (F3() " F2(y)) where y is Subset of F1() : P1[y]  }
then A2: x in dom F3() by FUNCT_1:def_7;
 F3() . x in union  {  F2(x) where x is Subset of F1() : P1[x]  }  by A1, FUNCT_1:def_7;
then consider y being set  such that
A3: F3() . x in y and
A4: y in  {  F2(x) where x is Subset of F1() : P1[x]  }  by TARSKI:def_4;
consider a being Subset of F1() such that
A5: y = F2(a) and
A6: P1[a] by A4;
A7: x in F3() " F2(a) by A2, A3, A5, FUNCT_1:def_7;
 F3() " F2(a) in  {  (F3() " F2(y)) where y is Subset of F1() : P1[y]  }  by A6;
hence  x in union  {  (F3() " F2(y)) where y is Subset of F1() : P1[y]  }  by A7, TARSKI:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union  {  (F3() " F2(y)) where y is Subset of F1() : P1[y]  }  or x in F3() " (union  {  F2(x) where x is Subset of F1() : P1[x]  }  ) )
assume  x in union  {  (F3() " F2(y)) where y is Subset of F1() : P1[y]  }  ; ::_thesis: x in F3() " (union  {  F2(x) where x is Subset of F1() : P1[x]  }  )
then consider y being set  such that
A8: x in y and
A9: y in  {  (F3() " F2(y)) where y is Subset of F1() : P1[y]  }  by TARSKI:def_4;
consider a being Subset of F1() such that
A10: y = F3() " F2(a) and
A11: P1[a] by A9;
A12: F3() . x in F2(a) by A8, A10, FUNCT_1:def_7;
 F2(a) in  {  F2(x) where x is Subset of F1() : P1[x]  }  by A11;
then A13: F3() . x in union  {  F2(x) where x is Subset of F1() : P1[x]  }  by A12, TARSKI:def_4;
 x in dom F3() by A8, A10, FUNCT_1:def_7;
hence  x in F3() " (union  {  F2(x) where x is Subset of F1() : P1[x]  }  ) by A13, FUNCT_1:def_7; ::_thesis: verum
end;

theorem Th2: :: YELLOW_9:2
for S being 1-sorted
for T being non empty 1-sorted
for f being Function of S,T
for X being Subset of T holds (f " X) ` = f " (X `)
proof
let S be 1-sorted ; ::_thesis: for T being non empty 1-sorted
for f being Function of S,T
for X being Subset of T holds (f " X) ` = f " (X `)
let T be non empty 1-sorted ; ::_thesis: for f being Function of S,T
for X being Subset of T holds (f " X) ` = f " (X `)
let f be Function of S,T; ::_thesis: for X being Subset of T holds (f " X) ` = f " (X `)
let X be Subset of T; ::_thesis: (f " X) ` = f " (X `)
thus (f " X) ` = the carrier of S \ (f " X) by SUBSET_1:def_4
.= (f " the carrier of T) \ (f " X) by FUNCT_2:40
.= f " ( the carrier of T \ X) by FUNCT_1:69
.= f " (X `) by SUBSET_1:def_4 ; ::_thesis: verum
end;

theorem Th3: :: YELLOW_9:3
for T being 1-sorted
for F being Subset-Family of T holds COMPLEMENT F =  {  (a `) where a is Subset of T : a in F  }
proof
let T be 1-sorted ; ::_thesis: for F being Subset-Family of T holds COMPLEMENT F =  {  (a `) where a is Subset of T : a in F  }
let F be Subset-Family of T; ::_thesis: COMPLEMENT F =  {  (a `) where a is Subset of T : a in F  }
set X =  {  (a `) where a is Subset of T : a in F  }  ;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  (a `) where a is Subset of T : a in F  }  c= COMPLEMENT F
let x be set ; ::_thesis: ( x in COMPLEMENT F implies x in  {  (a `) where a is Subset of T : a in F  }  )
assume A1: x in COMPLEMENT F ; ::_thesis: x in  {  (a `) where a is Subset of T : a in F  }
then reconsider P = x as Subset of T ;
A2: P ` in F by A1, SETFAM_1:def_7;
 (P `) ` = P ;
hence  x in  {  (a `) where a is Subset of T : a in F  }  by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (a `) where a is Subset of T : a in F  }  or x in COMPLEMENT F )
assume  x in  {  (a `) where a is Subset of T : a in F  }  ; ::_thesis: x in COMPLEMENT F
then  ex P being Subset of T st
( x = P ` & P in F ) ;
hence  x in COMPLEMENT F by YELLOW_8:5; ::_thesis: verum
end;

theorem Th4: :: YELLOW_9:4
for R being non empty RelStr
for F being Subset of R holds
( uparrow F = union  {  (uparrow x) where x is Element of R : x in F  }  & downarrow F = union  {  (downarrow x) where x is Element of R : x in F  }  )
proof
let R be non empty RelStr ; ::_thesis: for F being Subset of R holds
( uparrow F = union  {  (uparrow x) where x is Element of R : x in F  }  & downarrow F = union  {  (downarrow x) where x is Element of R : x in F  }  )
let F be Subset of R; ::_thesis: ( uparrow F = union  {  (uparrow x) where x is Element of R : x in F  }  & downarrow F = union  {  (downarrow x) where x is Element of R : x in F  }  )
A1: uparrow F =  {  x where x is Element of R : ex y being Element of R st
( x >= y & y in F )  }  by WAYBEL_0:15;
A2: downarrow F =  {  x where x is Element of R : ex y being Element of R st
( x <= y & y in F )  }  by WAYBEL_0:14;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: ( union  {  (uparrow x) where x is Element of R : x in F  }  c= uparrow F & downarrow F = union  {  (downarrow x) where x is Element of R : x in F  }  )
let a be set ; ::_thesis: ( a in uparrow F implies a in union  {  (uparrow z) where z is Element of R : z in F  }  )
assume  a in uparrow F ; ::_thesis: a in union  {  (uparrow z) where z is Element of R : z in F  }
then consider x being Element of R such that
A3: a = x and
A4: ex y being Element of R st
( x >= y & y in F ) by A1;
consider y being Element of R such that
A5: x >= y and
A6: y in F by A4;
A7: uparrow y in  {  (uparrow z) where z is Element of R : z in F  }  by A6;
 x in uparrow y by A5, WAYBEL_0:18;
hence  a in union  {  (uparrow z) where z is Element of R : z in F  }  by A3, A7, TARSKI:def_4; ::_thesis: verum
end;
hereby  :: according to TARSKI:def_3 ::_thesis: downarrow F = union  {  (downarrow x) where x is Element of R : x in F  }
let a be set ; ::_thesis: ( a in union  {  (uparrow x) where x is Element of R : x in F  }  implies a in uparrow F )
assume  a in union  {  (uparrow x) where x is Element of R : x in F  }  ; ::_thesis: a in uparrow F
then consider X being set  such that
A8: a in X and
A9: X in  {  (uparrow x) where x is Element of R : x in F  }  by TARSKI:def_4;
consider x being Element of R such that
A10: X = uparrow x and
A11: x in F by A9;
reconsider y = a as Element of R by A8, A10;
 y >= x by A8, A10, WAYBEL_0:18;
hence  a in uparrow F by A1, A11; ::_thesis: verum
end;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: union  {  (downarrow x) where x is Element of R : x in F  }  c= downarrow F
let a be set ; ::_thesis: ( a in downarrow F implies a in union  {  (downarrow z) where z is Element of R : z in F  }  )
assume  a in downarrow F ; ::_thesis: a in union  {  (downarrow z) where z is Element of R : z in F  }
then consider x being Element of R such that
A12: a = x and
A13: ex y being Element of R st
( x <= y & y in F ) by A2;
consider y being Element of R such that
A14: x <= y and
A15: y in F by A13;
A16: downarrow y in  {  (downarrow z) where z is Element of R : z in F  }  by A15;
 x in downarrow y by A14, WAYBEL_0:17;
hence  a in union  {  (downarrow z) where z is Element of R : z in F  }  by A12, A16, TARSKI:def_4; ::_thesis: verum
end;
hereby  :: according to TARSKI:def_3 ::_thesis: verum
let a be set ; ::_thesis: ( a in union  {  (downarrow x) where x is Element of R : x in F  }  implies a in downarrow F )
assume  a in union  {  (downarrow x) where x is Element of R : x in F  }  ; ::_thesis: a in downarrow F
then consider X being set  such that
A17: a in X and
A18: X in  {  (downarrow x) where x is Element of R : x in F  }  by TARSKI:def_4;
consider x being Element of R such that
A19: X = downarrow x and
A20: x in F by A18;
reconsider y = a as Element of R by A17, A19;
 y <= x by A17, A19, WAYBEL_0:17;
hence  a in downarrow F by A2, A20; ::_thesis: verum
end;
end;

theorem :: YELLOW_9:5
for R being non empty RelStr
for A being Subset-Family of R
for F being Subset of R st A =  {  ((uparrow x) `) where x is Element of R : x in F  }  holds
Intersect A = (uparrow F) `
proof
let R be non empty RelStr ; ::_thesis: for A being Subset-Family of R
for F being Subset of R st A =  {  ((uparrow x) `) where x is Element of R : x in F  }  holds
Intersect A = (uparrow F) `
deffunc H1( Element of R) ->  Element of bool the carrier of R = uparrow $1;
let A be Subset-Family of R; ::_thesis: for F being Subset of R st A =  {  ((uparrow x) `) where x is Element of R : x in F  }  holds
Intersect A = (uparrow F) `
let F be Subset of R; ::_thesis: ( A =  {  ((uparrow x) `) where x is Element of R : x in F  }  implies Intersect A = (uparrow F) ` )
assume A1: A =  {  (H1(x) `) where x is Element of R : x in F  }  ; ::_thesis: Intersect A = (uparrow F) `
A2: COMPLEMENT A =  {  H1(x) where x is Element of R : x in F  }  from YELLOW_9:sch_3(A1);
reconsider C = COMPLEMENT A as Subset-Family of R ;
 COMPLEMENT C = A ;
hence  Intersect A = (union C) ` by YELLOW_8:6
.= (uparrow F) ` by A2, Th4 ;
::_thesis: verum
end;

registration
cluster non empty 1 -element correct reflexive transitive antisymmetric with_suprema with_infima complete strict for TopRelStr ;
existence
 ex b1 being TopLattice st
( b1 is strict & b1 is complete & b1 is 1 -element )
proof
take  the finite 1 -element reflexive discrete strict TopRelStr ; ::_thesis: ( the finite 1 -element reflexive discrete strict TopRelStr is strict & the finite 1 -element reflexive discrete strict TopRelStr is complete & the finite 1 -element reflexive discrete strict TopRelStr is 1 -element )
thus  ( the finite 1 -element reflexive discrete strict TopRelStr is strict & the finite 1 -element reflexive discrete strict TopRelStr is complete & the finite 1 -element reflexive discrete strict TopRelStr is 1 -element ) ; ::_thesis: verum
end;
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric upper-bounded RelStr ;
cluster non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total infs-preserving for Element of bool [: the carrier of S, the carrier of T:];
existence
 ex b1 being Function of S,T st b1 is infs-preserving
proof
take f = S --> (Top T); ::_thesis: f is infs-preserving
let A be Subset of S; :: according to WAYBEL_0:def_32 ::_thesis: f preserves_inf_of A
assume  ex_inf_of A,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: A,T & "/\" ((f .: A),T) = f . ("/\" (A,S)) )
A1: rng f = {(Top T)} by FUNCOP_1:8;
 f .: A c= rng f by RELAT_1:111;
then A2: ( f .: A = {} or f .: A = {(Top T)} ) by A1, ZFMISC_1:33;
hence  ex_inf_of f .: A,T by YELLOW_0:38, YELLOW_0:43; ::_thesis: "/\" ((f .: A),T) = f . ("/\" (A,S))
thus  inf (f .: A) = Top T by A2, YELLOW_0:39
.= f . (inf A) by FUNCOP_1:7 ; ::_thesis: verum
end;
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive antisymmetric lower-bounded RelStr ;
cluster non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V27( the carrier of S) quasi_total sups-preserving for Element of bool [: the carrier of S, the carrier of T:];
existence
 ex b1 being Function of S,T st b1 is sups-preserving
proof
take f = S --> (Bottom T); ::_thesis: f is sups-preserving
let A be Subset of S; :: according to WAYBEL_0:def_33 ::_thesis: f preserves_sup_of A
assume  ex_sup_of A,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: A,T & sup (f .: A) = f . (sup A) )
A1: rng f = {(Bottom T)} by FUNCOP_1:8;
 f .: A c= rng f by RELAT_1:111;
then A2: ( f .: A = {} or f .: A = {(Bottom T)} ) by A1, ZFMISC_1:33;
hence  ex_sup_of f .: A,T by YELLOW_0:38, YELLOW_0:42; ::_thesis: sup (f .: A) = f . (sup A)
thus  sup (f .: A) = Bottom T by A2, YELLOW_0:39
.= f . (sup A) by FUNCOP_1:7 ; ::_thesis: verum
end;
end;

definition
let R, S be 1-sorted ;
assume A1: the carrier of S c= the carrier of R ;
A2: dom (id the carrier of S) = the carrier of S ;
A3: rng (id the carrier of S) = the carrier of S ;
func incl (S,R) ->  Function of S,R equals :Def1: :: YELLOW_9:def 1
 id the carrier of S;
coherence
 id the carrier of S is Function of S,R by A1, A2, A3, FUNCT_2:2;
end;

:: deftheorem Def1 defines incl YELLOW_9:def_1_:_
 for R, S being 1-sorted st the carrier of S c= the carrier of R holds
incl (S,R) = id the carrier of S;

registration
let R be non empty RelStr ;
let S be non empty SubRelStr of R;
cluster incl (S,R) ->  monotone ;
coherence
 incl (S,R) is monotone
proof
let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or (incl (S,R)) . x <= (incl (S,R)) . y )
reconsider a = x, b = y as Element of R by YELLOW_0:58;
 the carrier of S c= the carrier of R by YELLOW_0:def_13;
then A1: incl (S,R) = id the carrier of S by Def1;
then A2: (incl (S,R)) . x = a by FUNCT_1:18;
 (incl (S,R)) . y = b by A1, FUNCT_1:18;
hence  ( not x <= y or (incl (S,R)) . x <= (incl (S,R)) . y ) by A2, YELLOW_0:59; ::_thesis: verum
end;
end;

definition
let R be non empty RelStr ;
let X be non empty Subset of R;
funcX +id  ->  non empty strict NetStr over R equals :: YELLOW_9:def 2
(incl ((subrelstr X),R)) * ((subrelstr X) +id);
coherence
 (incl ((subrelstr X),R)) * ((subrelstr X) +id) is non empty strict NetStr over R ;
funcX opp+id  ->  non empty strict NetStr over R equals :: YELLOW_9:def 3
(incl ((subrelstr X),R)) * ((subrelstr X) opp+id);
coherence
 (incl ((subrelstr X),R)) * ((subrelstr X) opp+id) is non empty strict NetStr over R ;
end;

:: deftheorem  defines +id YELLOW_9:def_2_:_
 for R being non empty RelStr
for X being non empty Subset of R holds X +id = (incl ((subrelstr X),R)) * ((subrelstr X) +id);

:: deftheorem  defines opp+id YELLOW_9:def_3_:_
 for R being non empty RelStr
for X being non empty Subset of R holds X opp+id = (incl ((subrelstr X),R)) * ((subrelstr X) opp+id);

theorem :: YELLOW_9:6
for R being non empty RelStr
for X being non empty Subset of R holds
( the carrier of (X +id) = X & X +id is full SubRelStr of R & ( for x being Element of (X +id) holds (X +id) . x = x ) )
proof
let R be non empty RelStr ; ::_thesis: for X being non empty Subset of R holds
( the carrier of (X +id) = X & X +id is full SubRelStr of R & ( for x being Element of (X +id) holds (X +id) . x = x ) )
let X be non empty Subset of R; ::_thesis: ( the carrier of (X +id) = X & X +id is full SubRelStr of R & ( for x being Element of (X +id) holds (X +id) . x = x ) )
A1: RelStr(# the carrier of (X +id), the InternalRel of (X +id) #) = RelStr(# the carrier of ((subrelstr X) +id), the InternalRel of ((subrelstr X) +id) #) by WAYBEL_9:def_8;
A2: the mapping of (X +id) = (incl ((subrelstr X),R)) * the mapping of ((subrelstr X) +id) by WAYBEL_9:def_8;
A3: the carrier of (subrelstr X) = X by YELLOW_0:def_15;
hence A4: the carrier of (X +id) = X by A1, WAYBEL_9:def_5; ::_thesis: ( X +id is full SubRelStr of R & ( for x being Element of (X +id) holds (X +id) . x = x ) )
A5: RelStr(# the carrier of ((subrelstr X) +id), the InternalRel of ((subrelstr X) +id) #) = subrelstr X by WAYBEL_9:def_5;
 the InternalRel of (subrelstr X) c= the InternalRel of R by YELLOW_0:def_13;
then reconsider S = X +id as SubRelStr of R by A1, A3, A5, YELLOW_0:def_13;
 the InternalRel of S = the InternalRel of R |_2 the carrier of S by A1, A5, YELLOW_0:def_14;
hence  X +id is full SubRelStr of R by YELLOW_0:def_14; ::_thesis: for x being Element of (X +id) holds (X +id) . x = x
let x be Element of (X +id); ::_thesis: (X +id) . x = x
 id (subrelstr X) = id X by YELLOW_0:def_15;
then A6: the mapping of ((subrelstr X) +id) = id X by WAYBEL_9:def_5;
A7: dom (id X) = X ;
 incl ((subrelstr X),R) = id X by A3, Def1;
then  the mapping of (X +id) = id X by A2, A6, A7, RELAT_1:52;
hence  (X +id) . x = x by A4, FUNCT_1:18; ::_thesis: verum
end;

theorem :: YELLOW_9:7
for R being non empty RelStr
for X being non empty Subset of R holds
( the carrier of (X opp+id) = X & X opp+id is full SubRelStr of R opp & ( for x being Element of (X opp+id) holds (X opp+id) . x = x ) )
proof
let R be non empty RelStr ; ::_thesis: for X being non empty Subset of R holds
( the carrier of (X opp+id) = X & X opp+id is full SubRelStr of R opp & ( for x being Element of (X opp+id) holds (X opp+id) . x = x ) )
let X be non empty Subset of R; ::_thesis: ( the carrier of (X opp+id) = X & X opp+id is full SubRelStr of R opp & ( for x being Element of (X opp+id) holds (X opp+id) . x = x ) )
A1: RelStr(# the carrier of (X opp+id), the InternalRel of (X opp+id) #) = RelStr(# the carrier of ((subrelstr X) opp+id), the InternalRel of ((subrelstr X) opp+id) #) by WAYBEL_9:def_8;
A2: the mapping of (X opp+id) = (incl ((subrelstr X),R)) * the mapping of ((subrelstr X) opp+id) by WAYBEL_9:def_8;
A3: the carrier of (subrelstr X) = X by YELLOW_0:def_15;
A4: the carrier of ((subrelstr X) opp+id) = the carrier of (subrelstr X) by WAYBEL_9:def_6;
A5: the InternalRel of ((subrelstr X) opp+id) = the InternalRel of (subrelstr X) ~ by WAYBEL_9:def_6;
thus  the carrier of (X opp+id) = X by A1, A3, WAYBEL_9:def_6; ::_thesis: ( X opp+id is full SubRelStr of R opp & ( for x being Element of (X opp+id) holds (X opp+id) . x = x ) )
A6: R opp = RelStr(# the carrier of R,( the InternalRel of R ~) #) by LATTICE3:def_5;
 the InternalRel of (subrelstr X) = the InternalRel of R |_2 X by A3, YELLOW_0:def_14;
then A7: the InternalRel of ((subrelstr X) opp+id) = ( the InternalRel of R ~) |_2 X by A5, ORDERS_1:83;
then  the InternalRel of ((subrelstr X) opp+id) c= the InternalRel of (R opp) by A6, XBOOLE_1:17;
then reconsider S = X opp+id as SubRelStr of R opp by A1, A3, A4, A6, YELLOW_0:def_13;
 the InternalRel of S = the InternalRel of (R opp) |_2 the carrier of S by A1, A4, A6, A7, YELLOW_0:def_15;
hence  X opp+id is full SubRelStr of R opp by YELLOW_0:def_14; ::_thesis: for x being Element of (X opp+id) holds (X opp+id) . x = x
let x be Element of (X opp+id); ::_thesis: (X opp+id) . x = x
 id (subrelstr X) = id X by YELLOW_0:def_15;
then A8: the mapping of ((subrelstr X) opp+id) = id X by WAYBEL_9:def_6;
A9: dom (id X) = X ;
 incl ((subrelstr X),R) = id X by A3, Def1;
then  the mapping of (X opp+id) = id X by A2, A8, A9, RELAT_1:52;
hence  (X opp+id) . x = x by A1, A3, A4, FUNCT_1:18; ::_thesis: verum
end;

registration
let R be non empty reflexive RelStr ;
let X be non empty Subset of R;
clusterX +id  ->  non empty reflexive strict ;
coherence
 X +id is reflexive ;
clusterX opp+id  ->  non empty reflexive strict ;
coherence
 X opp+id is reflexive ;
end;

registration
let R be non empty transitive RelStr ;
let X be non empty Subset of R;
clusterX +id  ->  non empty transitive strict ;
coherence
 X +id is transitive ;
clusterX opp+id  ->  non empty transitive strict ;
coherence
 X opp+id is transitive ;
end;

registration
let R be non empty reflexive RelStr ;
let I be directed Subset of R;
cluster subrelstr I ->  directed ;
coherence
 subrelstr I is directed
proof
let x, y be Element of (subrelstr I); :: according to WAYBEL_0:def_1,WAYBEL_0:def_6 ::_thesis: ( not x in [#] (subrelstr I) or not y in [#] (subrelstr I) or ex b1 being Element of the carrier of (subrelstr I) st
( b1 in [#] (subrelstr I) & x <= b1 & y <= b1 ) )
A1: the carrier of (subrelstr I) = I by YELLOW_0:def_15;
assume that
A2: x in [#] (subrelstr I) and
A3: y in [#] (subrelstr I) ; ::_thesis: ex b1 being Element of the carrier of (subrelstr I) st
( b1 in [#] (subrelstr I) & x <= b1 & y <= b1 )
reconsider a = x, b = y as Element of R by A1, A2, A3;
consider c being Element of R such that
A4: c in I and
A5: a <= c and
A6: b <= c by A1, A2, WAYBEL_0:def_1;
reconsider z = c as Element of (subrelstr I) by A4, YELLOW_0:def_15;
take  z ; ::_thesis: ( z in [#] (subrelstr I) & x <= z & y <= z )
thus  ( z in [#] (subrelstr I) & x <= z & y <= z ) by A2, A5, A6, YELLOW_0:60; ::_thesis: verum
end;
end;

registration
let R be non empty reflexive RelStr ;
let I be non empty directed Subset of R;
clusterI +id  ->  non empty strict directed ;
coherence
 I +id is directed ;
end;

registration
let R be non empty reflexive RelStr ;
let F be non empty filtered Subset of R;
cluster(subrelstr F) opp+id  ->  directed ;
coherence
 (subrelstr F) opp+id is directed
proof
set I = F;
set A = (subrelstr F) opp+id ;
let x, y be Element of ((subrelstr F) opp+id); :: according to WAYBEL_0:def_1,WAYBEL_0:def_6 ::_thesis: ( not x in [#] ((subrelstr F) opp+id) or not y in [#] ((subrelstr F) opp+id) or ex b1 being Element of the carrier of ((subrelstr F) opp+id) st
( b1 in [#] ((subrelstr F) opp+id) & x <= b1 & y <= b1 ) )
A1: the carrier of (subrelstr F) = F by YELLOW_0:def_15;
A2: the carrier of ((subrelstr F) opp+id) = the carrier of (subrelstr F) by WAYBEL_9:def_6;
assume that
A3: x in [#] ((subrelstr F) opp+id) and
A4: y in [#] ((subrelstr F) opp+id) ; ::_thesis: ex b1 being Element of the carrier of ((subrelstr F) opp+id) st
( b1 in [#] ((subrelstr F) opp+id) & x <= b1 & y <= b1 )
reconsider a = x, b = y as Element of R by A1, A2, A3, A4;
A5: RelStr(# the carrier of ((subrelstr F) opp+id), the InternalRel of ((subrelstr F) opp+id) #) = RelStr(# the carrier of ((subrelstr F) opp), the InternalRel of ((subrelstr F) opp) #) by WAYBEL_9:11;
consider c being Element of R such that
A6: c in F and
A7: a >= c and
A8: b >= c by A1, A2, WAYBEL_0:def_2;
reconsider a1 = x, b1 = y, c1 = c as Element of (subrelstr F) by A6, WAYBEL_9:def_6, YELLOW_0:def_15;
reconsider z = c as Element of ((subrelstr F) opp+id) by A2, A6, YELLOW_0:def_15;
take  z ; ::_thesis: ( z in [#] ((subrelstr F) opp+id) & x <= z & y <= z )
A9: a1 ~ = a1 by LATTICE3:def_6;
A10: b1 ~ = b1 by LATTICE3:def_6;
A11: c1 ~ = c1 by LATTICE3:def_6;
A12: a1 >= c1 by A7, YELLOW_0:60;
A13: b1 >= c1 by A8, YELLOW_0:60;
A14: a1 ~ <= c1 ~ by A12, LATTICE3:9;
 b1 ~ <= c1 ~ by A13, LATTICE3:9;
hence  ( z in [#] ((subrelstr F) opp+id) & x <= z & y <= z ) by A5, A9, A10, A11, A14, YELLOW_0:1; ::_thesis: verum
end;
end;

registration
let R be non empty reflexive RelStr ;
let F be non empty filtered Subset of R;
clusterF opp+id  ->  non empty strict directed ;
coherence
 F opp+id is directed ;
end;

begin

theorem Th8: :: YELLOW_9:8
for T being TopSpace st T is empty holds
the topology of T = {{}}
proof
let T1 be TopSpace; ::_thesis: ( T1 is empty implies the topology of T1 = {{}} )
assume  T1 is empty ; ::_thesis: the topology of T1 = {{}}
then A1: the carrier of T1 = {} ;
then  {} in the topology of T1 by PRE_TOPC:def_1;
hence  the topology of T1 = {{}} by A1, ZFMISC_1:1, ZFMISC_1:33; ::_thesis: verum
end;

theorem Th9: :: YELLOW_9:9
for T being 1 -element TopSpace holds
( the topology of T = bool the carrier of T & ( for x being Point of T holds
( the carrier of T = {x} & the topology of T = {{},{x}} ) ) )
proof
let T be 1 -element TopSpace; ::_thesis: ( the topology of T = bool the carrier of T & ( for x being Point of T holds
( the carrier of T = {x} & the topology of T = {{},{x}} ) ) )
thus  the topology of T c= bool the carrier of T ; :: according to XBOOLE_0:def_10 ::_thesis: ( bool the carrier of T c= the topology of T & ( for x being Point of T holds
( the carrier of T = {x} & the topology of T = {{},{x}} ) ) )
consider x being Point of T such that
A1: the carrier of T = {x} by TEX_1:def_1;
A2: {} in the topology of T by PRE_TOPC:1;
A3: the carrier of T in the topology of T by PRE_TOPC:def_1;
A4: bool {x} = {{},{x}} by ZFMISC_1:24;
hence  bool the carrier of T c= the topology of T by A1, A2, A3, ZFMISC_1:32; ::_thesis: for x being Point of T holds
( the carrier of T = {x} & the topology of T = {{},{x}} )
let a be Point of T; ::_thesis: ( the carrier of T = {a} & the topology of T = {{},{a}} )
 a = x by STRUCT_0:def_10;
hence  ( the carrier of T = {a} & the topology of T c= {{},{a}} & {{},{a}} c= the topology of T ) by A1, A2, A3, A4, ZFMISC_1:32; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;

theorem :: YELLOW_9:10
for T being 1 -element TopSpace holds
( { the carrier of T} is Basis of T & {} is prebasis of T & {{}} is prebasis of T )
proof
let T be 1 -element TopSpace; ::_thesis: ( { the carrier of T} is Basis of T & {} is prebasis of T & {{}} is prebasis of T )
set BB = { the carrier of T};
A1: the carrier of T c= the carrier of T ;
A2: the topology of T = bool the carrier of T by Th9;
reconsider BB = { the carrier of T} as Subset-Family of T by A1, ZFMISC_1:31;
set x = the Element of T;
A3: the topology of T = {{},{ the Element of T}} by Th9;
A4: the carrier of T = { the Element of T} by Th9;
A5: {} c= bool the carrier of T by XBOOLE_1:2;
A6: {} c= BB by XBOOLE_1:2;
A7: {} c= the carrier of T by XBOOLE_1:2;
reconsider C = {} as Subset-Family of T by XBOOLE_1:2;
 the topology of T c= UniCl BB
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the topology of T or a in UniCl BB )
assume  a in the topology of T ; ::_thesis: a in UniCl BB
then  ( ( a = { the Element of T} & union {{ the Element of T}} = { the Element of T} & BB c= BB & BB c= bool the carrier of T ) or a = {} ) by A3, TARSKI:def_2, ZFMISC_1:25;
hence  a in UniCl BB by A4, A5, A6, A7, CANTOR_1:def_1, ZFMISC_1:2; ::_thesis: verum
end;
hence A8: { the carrier of T} is Basis of T by A2, CANTOR_1:def_2, TOPS_2:64; ::_thesis: ( {} is prebasis of T & {{}} is prebasis of T )
A9: {} c= the topology of T by XBOOLE_1:2;
 BB c= FinMeetCl C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in BB or x in FinMeetCl C )
assume  x in BB ; ::_thesis: x in FinMeetCl C
then  x = the carrier of T by TARSKI:def_1;
then  Intersect C = x by SETFAM_1:def_9;
hence  x in FinMeetCl C by CANTOR_1:def_3; ::_thesis: verum
end;
hence  {} is prebasis of T by A8, A9, CANTOR_1:def_4, TOPS_2:64; ::_thesis: {{}} is prebasis of T
 {} c= the carrier of T by XBOOLE_1:2;
then reconsider D = {{}} as Subset-Family of T by ZFMISC_1:31;
A10: D c= the topology of T by A3, ZFMISC_1:7;
 BB c= FinMeetCl D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in BB or x in FinMeetCl D )
assume  x in BB ; ::_thesis: x in FinMeetCl D
then A11: x = the carrier of T by TARSKI:def_1;
A12: Intersect C = the carrier of T by SETFAM_1:def_9;
 C c= D by XBOOLE_1:2;
hence  x in FinMeetCl D by A11, A12, CANTOR_1:def_3; ::_thesis: verum
end;
hence  {{}} is prebasis of T by A8, A10, CANTOR_1:def_4, TOPS_2:64; ::_thesis: verum
end;

theorem Th11: :: YELLOW_9:11
for X, Y being set
for A being Subset-Family of X st A = {Y} holds
( FinMeetCl A = {Y,X} & UniCl A = {Y,{}} )
proof
let X, Z be set ; ::_thesis: for A being Subset-Family of X st A = {Z} holds
( FinMeetCl A = {Z,X} & UniCl A = {Z,{}} )
let A be Subset-Family of X; ::_thesis: ( A = {Z} implies ( FinMeetCl A = {Z,X} & UniCl A = {Z,{}} ) )
assume A1: A = {Z} ; ::_thesis: ( FinMeetCl A = {Z,X} & UniCl A = {Z,{}} )
thus  FinMeetCl A c= {Z,X} :: according to XBOOLE_0:def_10 ::_thesis: ( {Z,X} c= FinMeetCl A & UniCl A = {Z,{}} )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in FinMeetCl A or x in {Z,X} )
assume  x in FinMeetCl A ; ::_thesis: x in {Z,X}
then consider Y being Subset-Family of X such that
A2: Y c= A and
 Y is finite and
A3: x = Intersect Y by CANTOR_1:def_3;
 ( Y = {} or Y = {Z} ) by A1, A2, ZFMISC_1:33;
then  ( x = X or x = meet {Z} ) by A3, SETFAM_1:def_9;
then  ( x = X or x = Z ) by SETFAM_1:10;
hence  x in {Z,X} by TARSKI:def_2; ::_thesis: verum
end;
reconsider E = {} as Subset-Family of X by XBOOLE_1:2;
reconsider E = E as Subset-Family of X ;
hereby  :: according to TARSKI:def_3 ::_thesis: UniCl A = {Z,{}}
let x be set ; ::_thesis: ( x in {Z,X} implies x in FinMeetCl A )
assume  x in {Z,X} ; ::_thesis: x in FinMeetCl A
then  ( x = X or x = Z ) by TARSKI:def_2;
then  ( x = X or x = meet {Z} ) by SETFAM_1:10;
then  ( ( x = Intersect E & E c= A ) or ( x = Intersect A & A c= A ) ) by A1, SETFAM_1:def_9, XBOOLE_1:2;
hence  x in FinMeetCl A by A1, CANTOR_1:def_3; ::_thesis: verum
end;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {Z,{}} c= UniCl A
let x be set ; ::_thesis: ( x in UniCl A implies x in {Z,{}} )
assume  x in UniCl A ; ::_thesis: x in {Z,{}}
then consider Y being Subset-Family of X such that
A4: Y c= A and
A5: x = union Y by CANTOR_1:def_1;
 ( Y = {} or Y = {Z} ) by A1, A4, ZFMISC_1:33;
then  ( x = {} or x = Z ) by A5, ZFMISC_1:2, ZFMISC_1:25;
hence  x in {Z,{}} by TARSKI:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {Z,{}} or x in UniCl A )
assume  x in {Z,{}} ; ::_thesis: x in UniCl A
then  ( x = {} or x = Z ) by TARSKI:def_2;
then  ( ( x = union E & E c= A ) or ( x = union A & A c= A ) ) by A1, XBOOLE_1:2, ZFMISC_1:2, ZFMISC_1:25;
hence  x in UniCl A by CANTOR_1:def_1; ::_thesis: verum
end;

theorem :: YELLOW_9:12
for X being set
for A, B being Subset-Family of X st ( A = B \/ {X} or B = A \ {X} ) holds
Intersect A = Intersect B
proof
let X be set ; ::_thesis: for A, B being Subset-Family of X st ( A = B \/ {X} or B = A \ {X} ) holds
Intersect A = Intersect B
let A, B be Subset-Family of X; ::_thesis: ( ( A = B \/ {X} or B = A \ {X} ) implies Intersect A = Intersect B )
assume A1: ( A = B \/ {X} or B = A \ {X} ) ; ::_thesis: Intersect A = Intersect B
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: Intersect B c= Intersect A
let x be set ; ::_thesis: ( x in Intersect A implies x in Intersect B )
assume A2: x in Intersect A ; ::_thesis: x in Intersect B
now__::_thesis:_for_y_being_set_st_y_in_B_holds_
x_in_y
let y be set ; ::_thesis: ( y in B implies x in y )
assume  y in B ; ::_thesis: x in y
then  y in A by A1, XBOOLE_0:def_3, XBOOLE_0:def_5;
hence  x in y by A2, SETFAM_1:43; ::_thesis: verum
end;
hence  x in Intersect B by A2, SETFAM_1:43; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersect B or x in Intersect A )
assume A3: x in Intersect B ; ::_thesis: x in Intersect A
now__::_thesis:_for_y_being_set_st_y_in_A_holds_
x_in_y
let y be set ; ::_thesis: ( y in A implies x in y )
assume  y in A ; ::_thesis: x in y
then  ( ( y in B & not y in {X} ) or y in {X} ) by A1, XBOOLE_0:def_3, XBOOLE_0:def_5;
then  ( y in B or y = X ) by TARSKI:def_1;
hence  x in y by A3, SETFAM_1:43; ::_thesis: verum
end;
hence  x in Intersect A by A3, SETFAM_1:43; ::_thesis: verum
end;

theorem :: YELLOW_9:13
for X being set
for A, B being Subset-Family of X st ( A = B \/ {X} or B = A \ {X} ) holds
FinMeetCl A = FinMeetCl B
proof
let X be set ; ::_thesis: for A, B being Subset-Family of X st ( A = B \/ {X} or B = A \ {X} ) holds
FinMeetCl A = FinMeetCl B
let A, B be Subset-Family of X; ::_thesis: ( ( A = B \/ {X} or B = A \ {X} ) implies FinMeetCl A = FinMeetCl B )
assume A1: ( A = B \/ {X} or B = A \ {X} ) ; ::_thesis: FinMeetCl A = FinMeetCl B
 X in FinMeetCl B by CANTOR_1:8;
then A2: {X} c= FinMeetCl B by ZFMISC_1:31;
A3: B c= FinMeetCl B by CANTOR_1:4;
 (A \ {X}) \/ {X} = A \/ {X} by XBOOLE_1:39;
then A4: A c= B \/ {X} by A1, XBOOLE_1:7;
 B \/ {X} c= FinMeetCl B by A2, A3, XBOOLE_1:8;
then  A c= FinMeetCl B by A4, XBOOLE_1:1;
then  FinMeetCl A c= FinMeetCl (FinMeetCl B) by CANTOR_1:14;
hence  FinMeetCl A c= FinMeetCl B by CANTOR_1:11; :: according to XBOOLE_0:def_10 ::_thesis: FinMeetCl B c= FinMeetCl A
thus  FinMeetCl B c= FinMeetCl A by A1, CANTOR_1:14, XBOOLE_1:7, XBOOLE_1:36; ::_thesis: verum
end;

theorem Th14: :: YELLOW_9:14
for X being set
for A being Subset-Family of X st X in A holds
for x being set holds
( x in FinMeetCl A iff ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) )
proof
let X be set ; ::_thesis: for A being Subset-Family of X st X in A holds
for x being set holds
( x in FinMeetCl A iff ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) )
let A be Subset-Family of X; ::_thesis: ( X in A implies for x being set holds
( x in FinMeetCl A iff ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) ) )
assume A1: X in A ; ::_thesis: for x being set holds
( x in FinMeetCl A iff ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) )
then A2: {X} c= A by ZFMISC_1:31;
reconsider Z = {X} as non empty finite Subset-Family of X by A1, ZFMISC_1:31;
reconsider Z = Z as non empty finite Subset-Family of X ;
A3: Intersect Z = meet Z by SETFAM_1:def_9
.= X by SETFAM_1:10 ;
let x be set ; ::_thesis: ( x in FinMeetCl A iff ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) )
hereby  ::_thesis: ( ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) implies x in FinMeetCl A )
assume  x in FinMeetCl A ; ::_thesis: ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y )
then consider Y being Subset-Family of X such that
A4: Y c= A and
A5: Y is finite and
A6: x = Intersect Y by CANTOR_1:def_3;
percases ( Y = {} or Y <> {} ) ;
suppose Y = {} ; ::_thesis: ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y )
then  x = X by A6, SETFAM_1:def_9;
hence  ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) by A2, A3; ::_thesis: verum
end;
suppose Y <> {} ; ::_thesis: ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y )
hence  ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) by A4, A5, A6; ::_thesis: verum
end;
end;
end;
thus  ( ex Y being non empty finite Subset-Family of X st
( Y c= A & x = Intersect Y ) implies x in FinMeetCl A ) by CANTOR_1:def_3; ::_thesis: verum
end;

theorem Th15: :: YELLOW_9:15
for X being set
for A being Subset-Family of X holds UniCl (UniCl A) = UniCl A
proof
let X be set ; ::_thesis: for A being Subset-Family of X holds UniCl (UniCl A) = UniCl A
let A be Subset-Family of X; ::_thesis: UniCl (UniCl A) = UniCl A
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: UniCl A c= UniCl (UniCl A)
let x be set ; ::_thesis: ( x in UniCl (UniCl A) implies x in UniCl A )
assume  x in UniCl (UniCl A) ; ::_thesis: x in UniCl A
then consider Y being Subset-Family of X such that
A1: Y c= UniCl A and
A2: x = union Y by CANTOR_1:def_1;
set Z =  {  y where y is Subset of X : ( y in A & y c= x )  }  ;
  {  y where y is Subset of X : ( y in A & y c= x )  }  c= bool X
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  y where y is Subset of X : ( y in A & y c= x )  }  or a in bool X )
assume  a in  {  y where y is Subset of X : ( y in A & y c= x )  }  ; ::_thesis: a in bool X
then  ex y being Subset of X st
( a = y & y in A & y c= x ) ;
hence  a in bool X ; ::_thesis: verum
end;
then reconsider Z =  {  y where y is Subset of X : ( y in A & y c= x )  }  as Subset-Family of X ;
A3: x = union Z
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: union Z c= x
let a be set ; ::_thesis: ( a in x implies a in union Z )
assume  a in x ; ::_thesis: a in union Z
then consider s being set  such that
A4: a in s and
A5: s in Y by A2, TARSKI:def_4;
consider t being Subset-Family of X such that
A6: t c= A and
A7: s = union t by A1, A5, CANTOR_1:def_1;
consider u being set  such that
A8: a in u and
A9: u in t by A4, A7, TARSKI:def_4;
reconsider u = u as Subset of X by A9;
A10: u c= s by A7, A9, ZFMISC_1:74;
 s c= x by A2, A5, ZFMISC_1:74;
then  u c= x by A10, XBOOLE_1:1;
then  u in Z by A6, A9;
hence  a in union Z by A8, TARSKI:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union Z or a in x )
assume  a in union Z ; ::_thesis: a in x
then consider u being set  such that
A11: a in u and
A12: u in Z by TARSKI:def_4;
 ex y being Subset of X st
( u = y & y in A & y c= x ) by A12;
hence  a in x by A11; ::_thesis: verum
end;
 Z c= A
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Z or a in A )
assume  a in Z ; ::_thesis: a in A
then  ex y being Subset of X st
( a = y & y in A & y c= x ) ;
hence  a in A ; ::_thesis: verum
end;
hence  x in UniCl A by A3, CANTOR_1:def_1; ::_thesis: verum
end;
thus  UniCl A c= UniCl (UniCl A) by CANTOR_1:1; ::_thesis: verum
end;

theorem Th16: :: YELLOW_9:16
for X being set
for A being empty Subset-Family of X holds UniCl A = {{}}
proof
let X be set ; ::_thesis: for A being empty Subset-Family of X holds UniCl A = {{}}
let A be empty Subset-Family of X; ::_thesis: UniCl A = {{}}
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= UniCl A
let x be set ; ::_thesis: ( x in UniCl A implies x in {{}} )
assume  x in UniCl A ; ::_thesis: x in {{}}
then consider B being Subset-Family of X such that
A1: B c= A and
A2: x = union B by CANTOR_1:def_1;
 B = {} by A1;
hence  x in {{}} by A2, TARSKI:def_1, ZFMISC_1:2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in UniCl A )
assume  x in {{}} ; ::_thesis: x in UniCl A
then A3: x = {} by TARSKI:def_1;
 union ({} (bool X)) = {} by ZFMISC_1:2;
hence  x in UniCl A by A3, CANTOR_1:def_1; ::_thesis: verum
end;

theorem Th17: :: YELLOW_9:17
for X being set
for A being empty Subset-Family of X holds FinMeetCl A = {X}
proof
let X be set ; ::_thesis: for A being empty Subset-Family of X holds FinMeetCl A = {X}
let A be empty Subset-Family of X; ::_thesis: FinMeetCl A = {X}
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {X} c= FinMeetCl A
let x be set ; ::_thesis: ( x in FinMeetCl A implies x in {X} )
assume  x in FinMeetCl A ; ::_thesis: x in {X}
then consider B being Subset-Family of X such that
A1: B c= A and
 B is finite and
A2: x = Intersect B by CANTOR_1:def_3;
 B = {} by A1;
then  x = X by A2, SETFAM_1:def_9;
hence  x in {X} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {X} or x in FinMeetCl A )
assume  x in {X} ; ::_thesis: x in FinMeetCl A
then A3: x = X by TARSKI:def_1;
 Intersect ({} (bool X)) = X by SETFAM_1:def_9;
hence  x in FinMeetCl A by A3, CANTOR_1:def_3; ::_thesis: verum
end;

theorem Th18: :: YELLOW_9:18
for X being set
for A being Subset-Family of X st A = {{},X} holds
( UniCl A = A & FinMeetCl A = A )
proof
let X be set ; ::_thesis: for A being Subset-Family of X st A = {{},X} holds
( UniCl A = A & FinMeetCl A = A )
let A be Subset-Family of X; ::_thesis: ( A = {{},X} implies ( UniCl A = A & FinMeetCl A = A ) )
assume A1: A = {{},X} ; ::_thesis: ( UniCl A = A & FinMeetCl A = A )
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: ( A c= UniCl A & FinMeetCl A = A )
let a be set ; ::_thesis: ( a in UniCl A implies a in A )
assume  a in UniCl A ; ::_thesis: a in A
then consider y being Subset-Family of X such that
A2: y c= A and
A3: a = union y by CANTOR_1:def_1;
 ( y = {} or y = {{}} or y = {X} or y = {{},X} ) by A1, A2, ZFMISC_1:36;
then  ( a = {} or a = X or ( a = {} \/ X & {} \/ X = X ) ) by A3, ZFMISC_1:2, ZFMISC_1:25, ZFMISC_1:75;
hence  a in A by A1, TARSKI:def_2; ::_thesis: verum
end;
thus  A c= UniCl A by CANTOR_1:1; ::_thesis: FinMeetCl A = A
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: A c= FinMeetCl A
let a be set ; ::_thesis: ( a in FinMeetCl A implies a in A )
assume  a in FinMeetCl A ; ::_thesis: a in A
then consider y being Subset-Family of X such that
A4: y c= A and
 y is finite and
A5: a = Intersect y by CANTOR_1:def_3;
 ( y = {} or y = {{}} or y = {X} or y = {{},X} ) by A1, A4, ZFMISC_1:36;
then  ( a = X or a = meet {{}} or a = meet {X} or a = meet {{},X} ) by A5, SETFAM_1:def_9;
then  ( a = X or a = {} or ( a = {} /\ X & {} /\ X = {} ) ) by SETFAM_1:10, SETFAM_1:11;
hence  a in A by A1, TARSKI:def_2; ::_thesis: verum
end;
thus  A c= FinMeetCl A by CANTOR_1:4; ::_thesis: verum
end;

theorem Th19: :: YELLOW_9:19
for X, Y being set
for A being Subset-Family of X
for B being Subset-Family of Y holds
( ( A c= B implies UniCl A c= UniCl B ) & ( A = B implies UniCl A = UniCl B ) )
proof
let X, Y be set ; ::_thesis: for A being Subset-Family of X
for B being Subset-Family of Y holds
( ( A c= B implies UniCl A c= UniCl B ) & ( A = B implies UniCl A = UniCl B ) )
let A be Subset-Family of X; ::_thesis: for B being Subset-Family of Y holds
( ( A c= B implies UniCl A c= UniCl B ) & ( A = B implies UniCl A = UniCl B ) )
let B be Subset-Family of Y; ::_thesis: ( ( A c= B implies UniCl A c= UniCl B ) & ( A = B implies UniCl A = UniCl B ) )
A1: now__::_thesis:_for_X,_Y_being_set_
for_A_being_Subset-Family_of_X
for_B_being_Subset-Family_of_Y_st_A_c=_B_holds_
UniCl_A_c=_UniCl_B
let X, Y be set ; ::_thesis: for A being Subset-Family of X
for B being Subset-Family of Y st A c= B holds
UniCl A c= UniCl B
let A be Subset-Family of X; ::_thesis: for B being Subset-Family of Y st A c= B holds
UniCl A c= UniCl B
let B be Subset-Family of Y; ::_thesis: ( A c= B implies UniCl A c= UniCl B )
assume A2: A c= B ; ::_thesis: UniCl A c= UniCl B
thus  UniCl A c= UniCl B ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UniCl A or x in UniCl B )
assume  x in UniCl A ; ::_thesis: x in UniCl B
then consider y being Subset-Family of X such that
A3: y c= A and
A4: x = union y by CANTOR_1:def_1;
 y c= B by A2, A3, XBOOLE_1:1;
then  y is Subset-Family of Y by XBOOLE_1:1;
then  ex y being Subset-Family of Y st
( y c= B & x = union y ) by A2, A3, A4, XBOOLE_1:1;
hence  x in UniCl B by CANTOR_1:def_1; ::_thesis: verum
end;
end;
hence  ( A c= B implies UniCl A c= UniCl B ) ; ::_thesis: ( A = B implies UniCl A = UniCl B )
assume  A = B ; ::_thesis: UniCl A = UniCl B
hence  ( UniCl A c= UniCl B & UniCl B c= UniCl A ) by A1; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;

theorem Th20: :: YELLOW_9:20
for X, Y being set
for A being Subset-Family of X
for B being Subset-Family of Y st A = B & X in A holds
FinMeetCl B = {Y} \/ (FinMeetCl A)
proof
let X, Y be set ; ::_thesis: for A being Subset-Family of X
for B being Subset-Family of Y st A = B & X in A holds
FinMeetCl B = {Y} \/ (FinMeetCl A)
let A be Subset-Family of X; ::_thesis: for B being Subset-Family of Y st A = B & X in A holds
FinMeetCl B = {Y} \/ (FinMeetCl A)
let B be Subset-Family of Y; ::_thesis: ( A = B & X in A implies FinMeetCl B = {Y} \/ (FinMeetCl A) )
assume that
A1: A = B and
A2: X in A ; ::_thesis: FinMeetCl B = {Y} \/ (FinMeetCl A)
thus  FinMeetCl B c= {Y} \/ (FinMeetCl A) :: according to XBOOLE_0:def_10 ::_thesis: {Y} \/ (FinMeetCl A) c= FinMeetCl B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in FinMeetCl B or x in {Y} \/ (FinMeetCl A) )
assume  x in FinMeetCl B ; ::_thesis: x in {Y} \/ (FinMeetCl A)
then consider y being Subset-Family of Y such that
A3: y c= B and
A4: y is finite and
A5: x = Intersect y by CANTOR_1:def_3;
reconsider z = y as Subset-Family of X by A1, A3, XBOOLE_1:1;
reconsider z = z as Subset-Family of X ;
percases ( y = {} or y <> {} ) ;
suppose y = {} ; ::_thesis: x in {Y} \/ (FinMeetCl A)
then  x = Y by A5, SETFAM_1:def_9;
then  x in {Y} by TARSKI:def_1;
hence  x in {Y} \/ (FinMeetCl A) by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA6: y <> {} ; ::_thesis: x in {Y} \/ (FinMeetCl A)
then A7: Intersect y = meet y by SETFAM_1:def_9;
 Intersect z = meet y by A6, SETFAM_1:def_9;
then  x in FinMeetCl A by A1, A3, A4, A5, A7, CANTOR_1:def_3;
hence  x in {Y} \/ (FinMeetCl A) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {Y} \/ (FinMeetCl A) or x in FinMeetCl B )
assume A8: x in {Y} \/ (FinMeetCl A) ; ::_thesis: x in FinMeetCl B
percases ( x in {Y} or x in FinMeetCl A ) by A8, XBOOLE_0:def_3;
suppose x in {Y} ; ::_thesis: x in FinMeetCl B
then A9: x = Y by TARSKI:def_1;
A10: Intersect ({} (bool Y)) = Y by SETFAM_1:def_9;
 {} (bool Y) c= B by XBOOLE_1:2;
hence  x in FinMeetCl B by A9, A10, CANTOR_1:def_3; ::_thesis: verum
end;
suppose x in FinMeetCl A ; ::_thesis: x in FinMeetCl B
then consider y being non empty finite Subset-Family of X such that
A11: y c= A and
A12: x = Intersect y by A2, Th14;
reconsider z = y as Subset-Family of Y by A1, A11, XBOOLE_1:1;
reconsider z = z as Subset-Family of Y ;
x = meet z by A12, SETFAM_1:def_9
.= Intersect z by SETFAM_1:def_9 ;
hence  x in FinMeetCl B by A1, A11, CANTOR_1:def_3; ::_thesis: verum
end;
end;
end;

theorem Th21: :: YELLOW_9:21
for X being set
for A being Subset-Family of X holds UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A)
proof
let X be set ; ::_thesis: for A being Subset-Family of X holds UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A)
let A be Subset-Family of X; ::_thesis: UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A)
percases ( A = {} or A <> {} ) ;
supposeA1: A = {} ; ::_thesis: UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A)
then A2: FinMeetCl A = {X} by Th17;
 UniCl A = {{}} by A1, Th16;
then A3: FinMeetCl (UniCl A) = {{},X} by Th11;
 UniCl (FinMeetCl A) = {X,{}} by A2, Th11;
hence  UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A) by A3, Th18; ::_thesis: verum
end;
suppose A <> {} ; ::_thesis: UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A)
then reconsider A = A as non empty Subset-Family of X ;
A4: UniCl (FinMeetCl (UniCl A)) c= UniCl (UniCl (FinMeetCl A))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UniCl (FinMeetCl (UniCl A)) or x in UniCl (UniCl (FinMeetCl A)) )
assume  x in UniCl (FinMeetCl (UniCl A)) ; ::_thesis: x in UniCl (UniCl (FinMeetCl A))
then consider Y being Subset-Family of X such that
A5: Y c= FinMeetCl (UniCl A) and
A6: x = union Y by CANTOR_1:def_1;
 Y c= UniCl (FinMeetCl A)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in UniCl (FinMeetCl A) )
assume  y in Y ; ::_thesis: y in UniCl (FinMeetCl A)
then consider Z being Subset-Family of X such that
A7: Z c= UniCl A and
A8: Z is finite and
A9: y = Intersect Z by A5, CANTOR_1:def_3;
percases ( Z = {} or Z <> {} ) ;
suppose Z = {} ; ::_thesis: y in UniCl (FinMeetCl A)
then  y = X by A9, SETFAM_1:def_9;
then A10: y in FinMeetCl A by CANTOR_1:8;
 FinMeetCl A c= UniCl (FinMeetCl A) by CANTOR_1:1;
hence  y in UniCl (FinMeetCl A) by A10; ::_thesis: verum
end;
supposeA11: Z <> {} ; ::_thesis: y in UniCl (FinMeetCl A)
then A12: y = meet Z by A9, SETFAM_1:def_9;
set G =  {  (meet (rng f)) where f is Element of Funcs (Z,A) : for z being set st z in Z holds
f . z c= z  }  ;
A13:  {  (meet (rng f)) where f is Element of Funcs (Z,A) : for z being set st z in Z holds
f . z c= z  }  c= FinMeetCl A
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (meet (rng f)) where f is Element of Funcs (Z,A) : for z being set st z in Z holds
f . z c= z  }  or a in FinMeetCl A )
assume  a in  {  (meet (rng f)) where f is Element of Funcs (Z,A) : for z being set st z in Z holds
f . z c= z  }  ; ::_thesis: a in FinMeetCl A
then consider f being Element of Funcs (Z,A) such that
A14: a = meet (rng f) and
 for z being set st z in Z holds
f . z c= z ;
reconsider B = rng f as Subset-Family of X by XBOOLE_1:1;
reconsider B = B as Subset-Family of X ;
 Intersect B = a by A11, A14, SETFAM_1:def_9;
hence  a in FinMeetCl A by A8, CANTOR_1:def_3; ::_thesis: verum
end;
then reconsider G =  {  (meet (rng f)) where f is Element of Funcs (Z,A) : for z being set st z in Z holds
f . z c= z  }  as Subset-Family of X by XBOOLE_1:1;
reconsider G = G as Subset-Family of X ;
 union G = y
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: y c= union G
let a be set ; ::_thesis: ( a in union G implies a in y )
assume  a in union G ; ::_thesis: a in y
then consider b being set  such that
A15: a in b and
A16: b in G by TARSKI:def_4;
consider f being Element of Funcs (Z,A) such that
A17: b = meet (rng f) and
A18: for z being set st z in Z holds
f . z c= z by A16;
A19: dom f = Z by FUNCT_2:def_1;
reconsider B = rng f as Subset-Family of X by XBOOLE_1:1;
reconsider B = B as Subset-Family of X ;
 b c= y
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in b or c in y )
assume A20: c in b ; ::_thesis: c in y
now__::_thesis:_for_d_being_set_st_d_in_Z_holds_
c_in_d
let d be set ; ::_thesis: ( d in Z implies c in d )
assume A21: d in Z ; ::_thesis: c in d
then  f . d in B by A19, FUNCT_1:def_3;
then A22: b c= f . d by A17, SETFAM_1:3;
A23: f . d c= d by A18, A21;
 c in f . d by A20, A22;
hence  c in d by A23; ::_thesis: verum
end;
hence  c in y by A11, A12, SETFAM_1:def_1; ::_thesis: verum
end;
hence  a in y by A15; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in y or a in union G )
assume A24: a in y ; ::_thesis: a in union G
defpred S1[ set , set ] means ( a in $2 & $2 c= $1 );
A25: now__::_thesis:_for_z_being_set_st_z_in_Z_holds_
ex_w_being_set_st_
(_w_in_A_&_S1[z,w]_)
let z be set ; ::_thesis: ( z in Z implies ex w being set st
( w in A & S1[z,w] ) )
assume A26: z in Z ; ::_thesis: ex w being set st
( w in A & S1[z,w] )
then A27: a in z by A12, A24, SETFAM_1:def_1;
consider C being Subset-Family of X such that
A28: C c= A and
A29: z = union C by A7, A26, CANTOR_1:def_1;
consider w being set  such that
A30: a in w and
A31: w in C by A27, A29, TARSKI:def_4;
take w = w; ::_thesis: ( w in A & S1[z,w] )
thus  w in A by A28, A31; ::_thesis: S1[z,w]
thus  S1[z,w] by A29, A30, A31, ZFMISC_1:74; ::_thesis: verum
end;
consider f being Function such that
A32: ( dom f = Z & rng f c= A ) and
A33: for z being set st z in Z holds
S1[z,f . z] from FUNCT_1:sch_5(A25);
reconsider f = f as Element of Funcs (Z,A) by A32, FUNCT_2:def_2;
 for z being set st z in Z holds
f . z c= z by A33;
then A34: meet (rng f) in G ;
now__::_thesis:_(_rng_f_<>_{}_&_(_for_y_being_set_st_y_in_rng_f_holds_
a_in_y_)_)
thus  rng f <> {} by A11; ::_thesis: for y being set st y in rng f holds
a in y
let y be set ; ::_thesis: ( y in rng f implies a in y )
assume  y in rng f ; ::_thesis: a in y
then  ex z being set st
( z in Z & y = f . z ) by A32, FUNCT_1:def_3;
hence  a in y by A33; ::_thesis: verum
end;
then  a in meet (rng f) by SETFAM_1:def_1;
hence  a in union G by A34, TARSKI:def_4; ::_thesis: verum
end;
hence  y in UniCl (FinMeetCl A) by A13, CANTOR_1:def_1; ::_thesis: verum
end;
end;
end;
hence  x in UniCl (UniCl (FinMeetCl A)) by A6, CANTOR_1:def_1; ::_thesis: verum
end;
 FinMeetCl A c= FinMeetCl (UniCl A) by CANTOR_1:1, CANTOR_1:14;
then A35: UniCl (FinMeetCl A) c= UniCl (FinMeetCl (UniCl A)) by CANTOR_1:9;
 UniCl (UniCl (FinMeetCl A)) = UniCl (FinMeetCl A) by Th15;
hence  UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A) by A4, A35, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
end;

begin

theorem Th22: :: YELLOW_9:22
for T being TopSpace
for K being Subset-Family of T holds
( the topology of T = UniCl K iff K is Basis of T )
proof
let T be TopSpace; ::_thesis: for K being Subset-Family of T holds
( the topology of T = UniCl K iff K is Basis of T )
let K be Subset-Family of T; ::_thesis: ( the topology of T = UniCl K iff K is Basis of T )
thus  ( the topology of T = UniCl K implies K is Basis of T ) ::_thesis: ( K is Basis of T implies the topology of T = UniCl K )
proof
assume  the topology of T = UniCl K ; ::_thesis: K is Basis of T
then  ( K c= the topology of T & the topology of T c= UniCl K ) by CANTOR_1:1;
hence  K is Basis of T by CANTOR_1:def_2, TOPS_2:64; ::_thesis: verum
end;
assume A1: K is Basis of T ; ::_thesis: the topology of T = UniCl K
then  K c= the topology of T by TOPS_2:64;
then A2: UniCl K c= UniCl the topology of T by CANTOR_1:9;
 the topology of T c= UniCl K by A1, CANTOR_1:def_2;
hence  ( the topology of T c= UniCl K & UniCl K c= the topology of T ) by A2, CANTOR_1:6; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;

theorem Th23: :: YELLOW_9:23
for T being TopSpace
for K being Subset-Family of T holds
( K is prebasis of T iff FinMeetCl K is Basis of T )
proof
let T be TopSpace; ::_thesis: for K being Subset-Family of T holds
( K is prebasis of T iff FinMeetCl K is Basis of T )
let BB be Subset-Family of T; ::_thesis: ( BB is prebasis of T iff FinMeetCl BB is Basis of T )
A1: now__::_thesis:_(_T_is_empty_implies_the_topology_of_T_=_bool_the_carrier_of_T_)
assume A2: T is empty ; ::_thesis: the topology of T = bool the carrier of T
then  the topology of T = {{}} by Th8;
hence  the topology of T = bool the carrier of T by A2, ZFMISC_1:1; ::_thesis: verum
end;
thus  ( BB is prebasis of T implies FinMeetCl BB is Basis of T ) ::_thesis: ( FinMeetCl BB is Basis of T implies BB is prebasis of T )
proof
assume A3: BB is prebasis of T ; ::_thesis: FinMeetCl BB is Basis of T
then  BB c= the topology of T by TOPS_2:64;
then  FinMeetCl BB c= FinMeetCl the topology of T by CANTOR_1:14;
then A4: FinMeetCl BB c= the topology of T by A1, CANTOR_1:5;
consider A being Basis of T such that
A5: A c= FinMeetCl BB by A3, CANTOR_1:def_4;
A6: the topology of T c= UniCl A by CANTOR_1:def_2;
 UniCl A c= UniCl (FinMeetCl BB) by A5, CANTOR_1:9;
then  the topology of T c= UniCl (FinMeetCl BB) by A6, XBOOLE_1:1;
hence  FinMeetCl BB is Basis of T by A4, CANTOR_1:def_2, TOPS_2:64; ::_thesis: verum
end;
assume A7: FinMeetCl BB is Basis of T ; ::_thesis: BB is prebasis of T
A8: BB c= FinMeetCl BB by CANTOR_1:4;
 FinMeetCl BB c= the topology of T by A7, TOPS_2:64;
then  BB c= the topology of T by A8, XBOOLE_1:1;
hence  BB is prebasis of T by A7, CANTOR_1:def_4, TOPS_2:64; ::_thesis: verum
end;

theorem Th24: :: YELLOW_9:24
for T being non empty TopSpace
for B being Subset-Family of T st UniCl B is prebasis of T holds
B is prebasis of T
proof
let T be non empty TopSpace; ::_thesis: for B being Subset-Family of T st UniCl B is prebasis of T holds
B is prebasis of T
let B be Subset-Family of T; ::_thesis: ( UniCl B is prebasis of T implies B is prebasis of T )
assume  UniCl B is prebasis of T ; ::_thesis: B is prebasis of T
then  FinMeetCl (UniCl B) is Basis of T by Th23;
then  UniCl (FinMeetCl (UniCl B)) = the topology of T by Th22;
then  UniCl (FinMeetCl B) = the topology of T by Th21;
then  FinMeetCl B is Basis of T by Th22;
hence  B is prebasis of T by Th23; ::_thesis: verum
end;

theorem Th25: :: YELLOW_9:25
for T1, T2 being TopSpace
for B being Basis of T1 st the carrier of T1 = the carrier of T2 & B is Basis of T2 holds
the topology of T1 = the topology of T2
proof
let T1, T2 be TopSpace; ::_thesis: for B being Basis of T1 st the carrier of T1 = the carrier of T2 & B is Basis of T2 holds
the topology of T1 = the topology of T2
let B be Basis of T1; ::_thesis: ( the carrier of T1 = the carrier of T2 & B is Basis of T2 implies the topology of T1 = the topology of T2 )
assume that
A1: the carrier of T1 = the carrier of T2 and
A2: B is Basis of T2 ; ::_thesis: the topology of T1 = the topology of T2
reconsider C = B as Basis of T2 by A2;
thus  the topology of T1 = UniCl C by A1, Th22
.= the topology of T2 by Th22 ; ::_thesis: verum
end;

theorem Th26: :: YELLOW_9:26
for T1, T2 being TopSpace
for P being prebasis of T1 st the carrier of T1 = the carrier of T2 & P is prebasis of T2 holds
the topology of T1 = the topology of T2
proof
let T1, T2 be TopSpace; ::_thesis: for P being prebasis of T1 st the carrier of T1 = the carrier of T2 & P is prebasis of T2 holds
the topology of T1 = the topology of T2
let P be prebasis of T1; ::_thesis: ( the carrier of T1 = the carrier of T2 & P is prebasis of T2 implies the topology of T1 = the topology of T2 )
assume that
A1: the carrier of T1 = the carrier of T2 and
A2: P is prebasis of T2 ; ::_thesis: the topology of T1 = the topology of T2
reconsider C = P as prebasis of T2 by A2;
A3: FinMeetCl P is Basis of T1 by Th23;
 FinMeetCl C is Basis of T2 by Th23;
hence  the topology of T1 = the topology of T2 by A1, A3, Th25; ::_thesis: verum
end;

theorem :: YELLOW_9:27
for T being TopSpace
for K being Basis of T holds
( K is open & K is prebasis of T ) ;

theorem :: YELLOW_9:28
for T being TopSpace
for K being prebasis of T holds K is open ;

theorem Th29: :: YELLOW_9:29
for T being non empty TopSpace
for B being prebasis of T holds B \/ { the carrier of T} is prebasis of T
proof
let T be non empty TopSpace; ::_thesis: for B being prebasis of T holds B \/ { the carrier of T} is prebasis of T
let B be prebasis of T; ::_thesis: B \/ { the carrier of T} is prebasis of T
set C = B \/ { the carrier of T};
A1: the carrier of T in the topology of T by PRE_TOPC:def_1;
A2: B c= the topology of T by TOPS_2:64;
A3: { the carrier of T} c= the topology of T by A1, ZFMISC_1:31;
then  B \/ { the carrier of T} c= the topology of T by A2, XBOOLE_1:8;
then reconsider C = B \/ { the carrier of T} as Subset-Family of T by XBOOLE_1:1;
A4: C c= the topology of T by A2, A3, XBOOLE_1:8;
A5: FinMeetCl B c= FinMeetCl C by CANTOR_1:14, XBOOLE_1:7;
 FinMeetCl B is Basis of T by Th23;
hence  B \/ { the carrier of T} is prebasis of T by A4, A5, CANTOR_1:def_4, TOPS_2:64; ::_thesis: verum
end;

theorem :: YELLOW_9:30
for T being TopSpace
for B being Basis of T holds B \/ { the carrier of T} is Basis of T
proof
let T be TopSpace; ::_thesis: for B being Basis of T holds B \/ { the carrier of T} is Basis of T
let B be Basis of T; ::_thesis: B \/ { the carrier of T} is Basis of T
set C = B \/ { the carrier of T};
A1: the carrier of T in the topology of T by PRE_TOPC:def_1;
A2: B c= the topology of T by TOPS_2:64;
A3: { the carrier of T} c= the topology of T by A1, ZFMISC_1:31;
then  B \/ { the carrier of T} c= the topology of T by A2, XBOOLE_1:8;
then reconsider C = B \/ { the carrier of T} as Subset-Family of T by XBOOLE_1:1;
A4: C c= the topology of T by A2, A3, XBOOLE_1:8;
A5: UniCl B c= UniCl C by CANTOR_1:9, XBOOLE_1:7;
 the topology of T c= UniCl B by CANTOR_1:def_2;
then  the topology of T c= UniCl C by A5, XBOOLE_1:1;
hence  B \/ { the carrier of T} is Basis of T by A4, CANTOR_1:def_2, TOPS_2:64; ::_thesis: verum
end;

theorem Th31: :: YELLOW_9:31
for T being TopSpace
for B being Basis of T
for A being Subset of T holds
( A is open iff for p being Point of T st p in A holds
ex a being Subset of T st
( a in B & p in a & a c= A ) )
proof
let T be TopSpace; ::_thesis: for B being Basis of T
for A being Subset of T holds
( A is open iff for p being Point of T st p in A holds
ex a being Subset of T st
( a in B & p in a & a c= A ) )
let K be Basis of T; ::_thesis: for A being Subset of T holds
( A is open iff for p being Point of T st p in A holds
ex a being Subset of T st
( a in K & p in a & a c= A ) )
let A be Subset of T; ::_thesis: ( A is open iff for p being Point of T st p in A holds
ex a being Subset of T st
( a in K & p in a & a c= A ) )
hereby  ::_thesis: ( ( for p being Point of T st p in A holds
ex a being Subset of T st
( a in K & p in a & a c= A ) ) implies A is open )
assume  A is open ; ::_thesis: for p being Point of T st p in A holds
ex a being Subset of T st
( a in K & p in a & a c= A )
then A1: A = union  {  G where G is Subset of T : ( G in K & G c= A )  }  by YELLOW_8:9;
let p be Point of T; ::_thesis: ( p in A implies ex a being Subset of T st
( a in K & p in a & a c= A ) )
assume  p in A ; ::_thesis: ex a being Subset of T st
( a in K & p in a & a c= A )
then consider Z being set  such that
A2: p in Z and
A3: Z in  {  G where G is Subset of T : ( G in K & G c= A )  }  by A1, TARSKI:def_4;
 ex a being Subset of T st
( Z = a & a in K & a c= A ) by A3;
hence  ex a being Subset of T st
( a in K & p in a & a c= A ) by A2; ::_thesis: verum
end;
assume A4: for p being Point of T st p in A holds
ex a being Subset of T st
( a in K & p in a & a c= A ) ; ::_thesis: A is open
set F =  {  G where G is Subset of T : ( G in K & G c= A )  }  ;
  {  G where G is Subset of T : ( G in K & G c= A )  }  c= bool the carrier of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  G where G is Subset of T : ( G in K & G c= A )  }  or x in bool the carrier of T )
assume  x in  {  G where G is Subset of T : ( G in K & G c= A )  }  ; ::_thesis: x in bool the carrier of T
then  ex G being Subset of T st
( x = G & G in K & G c= A ) ;
hence  x in bool the carrier of T ; ::_thesis: verum
end;
then reconsider F =  {  G where G is Subset of T : ( G in K & G c= A )  }  as Subset-Family of T ;
reconsider F = F as Subset-Family of T ;
A5: F is open
proof
let x be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not x in F or x is open )
assume  x in F ; ::_thesis: x is open
then A6: ex G being Subset of T st
( x = G & G in K & G c= A ) ;
 K c= the topology of T by TOPS_2:64;
hence  x in the topology of T by A6; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
 A = union F
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: union F c= A
let x be set ; ::_thesis: ( x in A implies x in union F )
assume A7: x in A ; ::_thesis: x in union F
then reconsider p = x as Point of T ;
consider a being Subset of T such that
A8: a in K and
A9: p in a and
A10: a c= A by A4, A7;
 a in F by A8, A10;
hence  x in union F by A9, TARSKI:def_4; ::_thesis: verum
end;
 F c= bool A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in bool A )
assume  x in F ; ::_thesis: x in bool A
then  ex G being Subset of T st
( x = G & G in K & G c= A ) ;
hence  x in bool A ; ::_thesis: verum
end;
then  union F c= union (bool A) by ZFMISC_1:77;
hence  union F c= A by ZFMISC_1:81; ::_thesis: verum
end;
hence  A is open by A5, TOPS_2:19; ::_thesis: verum
end;

theorem Th32: :: YELLOW_9:32
for T being TopSpace
for B being Subset-Family of T st B c= the topology of T & ( for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B & p in a & a c= A ) ) holds
B is Basis of T
proof
let T be TopSpace; ::_thesis: for B being Subset-Family of T st B c= the topology of T & ( for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B & p in a & a c= A ) ) holds
B is Basis of T
let B be Subset-Family of T; ::_thesis: ( B c= the topology of T & ( for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B & p in a & a c= A ) ) implies B is Basis of T )
assume that
A1: B c= the topology of T and
A2: for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B & p in a & a c= A ) ; ::_thesis: B is Basis of T
A3: B is open by A1, TOPS_2:64;
 B is quasi_basis
proof
let x be set ; :: according to TARSKI:def_3,CANTOR_1:def_2 ::_thesis: ( not x in the topology of T or x in UniCl B )
assume A4: x in the topology of T ; ::_thesis: x in UniCl B
then reconsider A = x as Subset of T ;
set Y =  {  V where V is Subset of T : ( V in B & V c= A )  }  ;
  {  V where V is Subset of T : ( V in B & V c= A )  }  c= bool the carrier of T
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  V where V is Subset of T : ( V in B & V c= A )  }  or y in bool the carrier of T )
assume  y in  {  V where V is Subset of T : ( V in B & V c= A )  }  ; ::_thesis: y in bool the carrier of T
then  ex V being Subset of T st
( y = V & V in B & V c= A ) ;
hence  y in bool the carrier of T ; ::_thesis: verum
end;
then reconsider Y =  {  V where V is Subset of T : ( V in B & V c= A )  }  as Subset-Family of T ;
A5: Y c= B
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in B )
assume  y in Y ; ::_thesis: y in B
then  ex V being Subset of T st
( y = V & V in B & V c= A ) ;
hence  y in B ; ::_thesis: verum
end;
 x = union Y
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: union Y c= x
let p be set ; ::_thesis: ( p in x implies p in union Y )
assume A6: p in x ; ::_thesis: p in union Y
then  p in A ;
then reconsider q = p as Point of T ;
 A is open by A4, PRE_TOPC:def_2;
then consider a being Subset of T such that
A7: a in B and
A8: q in a and
A9: a c= A by A2, A6;
 a in Y by A7, A9;
hence  p in union Y by A8, TARSKI:def_4; ::_thesis: verum
end;
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in union Y or p in x )
assume  p in union Y ; ::_thesis: p in x
then consider a being set  such that
A10: p in a and
A11: a in Y by TARSKI:def_4;
 ex V being Subset of T st
( a = V & V in B & V c= A ) by A11;
hence  p in x by A10; ::_thesis: verum
end;
hence  x in UniCl B by A5, CANTOR_1:def_1; ::_thesis: verum
end;
hence  B is Basis of T by A3; ::_thesis: verum
end;

theorem Th33: :: YELLOW_9:33
for S being TopSpace
for T being non empty TopSpace
for K being Basis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " (A `) is closed )
proof
let S be TopSpace; ::_thesis: for T being non empty TopSpace
for K being Basis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " (A `) is closed )
let T be non empty TopSpace; ::_thesis: for K being Basis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " (A `) is closed )
let BB be Basis of T; ::_thesis: for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in BB holds
f " (A `) is closed )
let f be Function of S,T; ::_thesis: ( f is continuous iff for A being Subset of T st A in BB holds
f " (A `) is closed )
A1: BB c= the topology of T by TOPS_2:64;
hereby  ::_thesis: ( ( for A being Subset of T st A in BB holds
f " (A `) is closed ) implies f is continuous )
assume A2: f is continuous ; ::_thesis: for A being Subset of T st A in BB holds
f " (A `) is closed
let A be Subset of T; ::_thesis: ( A in BB implies f " (A `) is closed )
assume  A in BB ; ::_thesis: f " (A `) is closed
then  A is open by A1, PRE_TOPC:def_2;
then  A ` is closed by TOPS_1:4;
hence  f " (A `) is closed by A2, PRE_TOPC:def_6; ::_thesis: verum
end;
assume A3: for A being Subset of T st A in BB holds
f " (A `) is closed ; ::_thesis: f is continuous
let A be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( not A is closed or f " A is closed )
assume  A is closed ; ::_thesis: f " A is closed
then  A ` is open by TOPS_1:3;
then A4: A ` = union  {  G where G is Subset of T : ( G in BB & G c= A ` )  }  by YELLOW_8:9;
set F =  {  (f " G) where G is Subset of T : ( G in BB & G c= A ` )  }  ;
  {  (f " G) where G is Subset of T : ( G in BB & G c= A ` )  }  c= bool the carrier of S
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (f " G) where G is Subset of T : ( G in BB & G c= A ` )  }  or a in bool the carrier of S )
assume  a in  {  (f " G) where G is Subset of T : ( G in BB & G c= A ` )  }  ; ::_thesis: a in bool the carrier of S
then  ex G being Subset of T st
( a = f " G & G in BB & G c= A ` ) ;
hence  a in bool the carrier of S ; ::_thesis: verum
end;
then reconsider F =  {  (f " G) where G is Subset of T : ( G in BB & G c= A ` )  }  as Subset-Family of S ;
reconsider F = F as Subset-Family of S ;
 F c= the topology of S
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in F or a in the topology of S )
assume  a in F ; ::_thesis: a in the topology of S
then consider G being Subset of T such that
A5: a = f " G and
A6: G in BB and
 G c= A ` ;
A7: f " (G `) is closed by A3, A6;
 (f " G) ` = f " (G `) by Th2;
then  f " G is open by A7, TOPS_1:4;
hence  a in the topology of S by A5, PRE_TOPC:def_2; ::_thesis: verum
end;
then A8: union F in the topology of S by PRE_TOPC:def_1;
defpred S1[ Subset of T] means ( $1 in BB & $1 c= A ` );
deffunc H1( Subset of T) ->  Subset of T = $1;
 f " (union  {  H1(G) where G is Subset of T : S1[G]  }  ) = union  {  (f " H1(G)) where G is Subset of T : S1[G]  }  from YELLOW_9:sch_4();
then  f " (A `) is open by A4, A8, PRE_TOPC:def_2;
then  (f " A) ` is open by Th2;
hence  f " A is closed by TOPS_1:3; ::_thesis: verum
end;

theorem :: YELLOW_9:34
for S being TopSpace
for T being non empty TopSpace
for K being Basis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " A is open )
proof
let S be TopSpace; ::_thesis: for T being non empty TopSpace
for K being Basis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " A is open )
let T be non empty TopSpace; ::_thesis: for K being Basis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " A is open )
let K be Basis of T; ::_thesis: for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " A is open )
let f be Function of S,T; ::_thesis: ( f is continuous iff for A being Subset of T st A in K holds
f " A is open )
hereby  ::_thesis: ( ( for A being Subset of T st A in K holds
f " A is open ) implies f is continuous )
assume A1: f is continuous ; ::_thesis: for A being Subset of T st A in K holds
f " A is open
let A be Subset of T; ::_thesis: ( A in K implies f " A is open )
assume  A in K ; ::_thesis: f " A is open
then  f " (A `) is closed by A1, Th33;
then  (f " A) ` is closed by Th2;
hence  f " A is open by TOPS_1:4; ::_thesis: verum
end;
assume A2: for A being Subset of T st A in K holds
f " A is open ; ::_thesis: f is continuous
now__::_thesis:_for_A_being_Subset_of_T_st_A_in_K_holds_
f_"_(A_`)_is_closed
let A be Subset of T; ::_thesis: ( A in K implies f " (A `) is closed )
assume  A in K ; ::_thesis: f " (A `) is closed
then  f " A is open by A2;
then  (f " A) ` is closed by TOPS_1:4;
hence  f " (A `) is closed by Th2; ::_thesis: verum
end;
hence  f is continuous by Th33; ::_thesis: verum
end;

theorem Th35: :: YELLOW_9:35
for S being TopSpace
for T being non empty TopSpace
for K being prebasis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " (A `) is closed )
proof
let S be TopSpace; ::_thesis: for T being non empty TopSpace
for K being prebasis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " (A `) is closed )
let T be non empty TopSpace; ::_thesis: for K being prebasis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " (A `) is closed )
let BB be prebasis of T; ::_thesis: for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in BB holds
f " (A `) is closed )
let f be Function of S,T; ::_thesis: ( f is continuous iff for A being Subset of T st A in BB holds
f " (A `) is closed )
A1: BB c= the topology of T by TOPS_2:64;
hereby  ::_thesis: ( ( for A being Subset of T st A in BB holds
f " (A `) is closed ) implies f is continuous )
assume A2: f is continuous ; ::_thesis: for A being Subset of T st A in BB holds
f " (A `) is closed
let A be Subset of T; ::_thesis: ( A in BB implies f " (A `) is closed )
assume  A in BB ; ::_thesis: f " (A `) is closed
then  A is open by A1, PRE_TOPC:def_2;
then  A ` is closed by TOPS_1:4;
hence  f " (A `) is closed by A2, PRE_TOPC:def_6; ::_thesis: verum
end;
assume A3: for A being Subset of T st A in BB holds
f " (A `) is closed ; ::_thesis: f is continuous
reconsider C = FinMeetCl BB as Basis of T by Th23;
now__::_thesis:_for_A_being_Subset_of_T_st_A_in_C_holds_
f_"_(A_`)_is_closed
let A be Subset of T; ::_thesis: ( A in C implies f " (A `) is closed )
assume  A in C ; ::_thesis: f " (A `) is closed
then consider Y being Subset-Family of T such that
A4: Y c= BB and
A5: Y is finite and
A6: A = Intersect Y by CANTOR_1:def_3;
reconsider Y = Y as Subset-Family of T ;
reconsider CY = COMPLEMENT Y as Subset-Family of T ;
defpred S1[ set ] means $1 in Y;
deffunc H1( Subset of T) ->  Element of bool the carrier of T = $1 ` ;
A7: f " (A `) = f " (union CY) by A6, YELLOW_8:7
.= f " (union  {  H1(a) where a is Subset of T : S1[a]  }  ) by Th3
.= union  {  (f " H1(y)) where y is Subset of T : S1[y]  }  from YELLOW_9:sch_4() ;
set X =  {  (f " (y `)) where y is Subset of T : y in Y  }  ;
  {  (f " (y `)) where y is Subset of T : y in Y  }  c= bool the carrier of S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (f " (y `)) where y is Subset of T : y in Y  }  or x in bool the carrier of S )
assume  x in  {  (f " (y `)) where y is Subset of T : y in Y  }  ; ::_thesis: x in bool the carrier of S
then  ex y being Subset of T st
( x = f " (y `) & y in Y ) ;
hence  x in bool the carrier of S ; ::_thesis: verum
end;
then reconsider X =  {  (f " (y `)) where y is Subset of T : y in Y  }  as Subset-Family of S ;
reconsider X = X as Subset-Family of S ;
A8: X is closed
proof
let a be Subset of S; :: according to TOPS_2:def_2 ::_thesis: ( not a in X or a is closed )
assume  a in X ; ::_thesis: a is closed
then  ex y being Subset of T st
( a = f " (y `) & y in Y ) ;
hence  a is closed by A3, A4; ::_thesis: verum
end;
A9: Y is finite by A5;
deffunc H2( Subset of T) ->  Element of bool the carrier of S = f " ($1 `);
  {  H2(y) where y is Subset of T : y in Y  }  is finite from FRAENKEL:sch_21(A9);
hence  f " (A `) is closed by A7, A8, TOPS_2:21; ::_thesis: verum
end;
hence  f is continuous by Th33; ::_thesis: verum
end;

theorem :: YELLOW_9:36
for S being TopSpace
for T being non empty TopSpace
for K being prebasis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " A is open )
proof
let S be TopSpace; ::_thesis: for T being non empty TopSpace
for K being prebasis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " A is open )
let T be non empty TopSpace; ::_thesis: for K being prebasis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " A is open )
let K be prebasis of T; ::_thesis: for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " A is open )
let f be Function of S,T; ::_thesis: ( f is continuous iff for A being Subset of T st A in K holds
f " A is open )
hereby  ::_thesis: ( ( for A being Subset of T st A in K holds
f " A is open ) implies f is continuous )
assume A1: f is continuous ; ::_thesis: for A being Subset of T st A in K holds
f " A is open
let A be Subset of T; ::_thesis: ( A in K implies f " A is open )
assume  A in K ; ::_thesis: f " A is open
then  f " (A `) is closed by A1, Th35;
then  (f " A) ` is closed by Th2;
hence  f " A is open by TOPS_1:4; ::_thesis: verum
end;
assume A2: for A being Subset of T st A in K holds
f " A is open ; ::_thesis: f is continuous
now__::_thesis:_for_A_being_Subset_of_T_st_A_in_K_holds_
f_"_(A_`)_is_closed
let A be Subset of T; ::_thesis: ( A in K implies f " (A `) is closed )
assume  A in K ; ::_thesis: f " (A `) is closed
then  f " A is open by A2;
then  (f " A) ` is closed by TOPS_1:4;
hence  f " (A `) is closed by Th2; ::_thesis: verum
end;
hence  f is continuous by Th35; ::_thesis: verum
end;

theorem Th37: :: YELLOW_9:37
for T being non empty TopSpace
for x being Point of T
for X being Subset of T
for K being Basis of T st ( for A being Subset of T st A in K & x in A holds
A meets X ) holds
x in Cl X
proof
let T be non empty TopSpace; ::_thesis: for x being Point of T
for X being Subset of T
for K being Basis of T st ( for A being Subset of T st A in K & x in A holds
A meets X ) holds
x in Cl X
let x be Point of T; ::_thesis: for X being Subset of T
for K being Basis of T st ( for A being Subset of T st A in K & x in A holds
A meets X ) holds
x in Cl X
let X be Subset of T; ::_thesis: for K being Basis of T st ( for A being Subset of T st A in K & x in A holds
A meets X ) holds
x in Cl X
let BB be Basis of T; ::_thesis: ( ( for A being Subset of T st A in BB & x in A holds
A meets X ) implies x in Cl X )
assume A1: for A being Subset of T st A in BB & x in A holds
A meets X ; ::_thesis: x in Cl X
now__::_thesis:_for_G_being_a_neighborhood_of_x_holds_G_meets_X
let G be a_neighborhood of x; ::_thesis: G meets X
A2: Int G = union  {  A where A is Subset of T : ( A in BB & A c= G )  }  by YELLOW_8:11;
 x in Int G by CONNSP_2:def_1;
then consider Z being set  such that
A3: x in Z and
A4: Z in  {  A where A is Subset of T : ( A in BB & A c= G )  }  by A2, TARSKI:def_4;
 ex A being Subset of T st
( Z = A & A in BB & A c= G ) by A4;
hence  G meets X by A1, A3, XBOOLE_1:63; ::_thesis: verum
end;
hence  x in Cl X by CONNSP_2:27; ::_thesis: verum
end;

theorem Th38: :: YELLOW_9:38
for T being non empty TopSpace
for x being Point of T
for X being Subset of T
for K being prebasis of T st ( for Z being finite Subset-Family of T st Z c= K & x in Intersect Z holds
Intersect Z meets X ) holds
x in Cl X
proof
let T be non empty TopSpace; ::_thesis: for x being Point of T
for X being Subset of T
for K being prebasis of T st ( for Z being finite Subset-Family of T st Z c= K & x in Intersect Z holds
Intersect Z meets X ) holds
x in Cl X
let x be Point of T; ::_thesis: for X being Subset of T
for K being prebasis of T st ( for Z being finite Subset-Family of T st Z c= K & x in Intersect Z holds
Intersect Z meets X ) holds
x in Cl X
let X be Subset of T; ::_thesis: for K being prebasis of T st ( for Z being finite Subset-Family of T st Z c= K & x in Intersect Z holds
Intersect Z meets X ) holds
x in Cl X
let BB be prebasis of T; ::_thesis: ( ( for Z being finite Subset-Family of T st Z c= BB & x in Intersect Z holds
Intersect Z meets X ) implies x in Cl X )
assume A1: for Z being finite Subset-Family of T st Z c= BB & x in Intersect Z holds
Intersect Z meets X ; ::_thesis: x in Cl X
reconsider BB9 = FinMeetCl BB as Basis of T by Th23;
now__::_thesis:_for_A_being_Subset_of_T_st_A_in_BB9_&_x_in_A_holds_
A_meets_X
let A be Subset of T; ::_thesis: ( A in BB9 & x in A implies A meets X )
assume  A in BB9 ; ::_thesis: ( x in A implies A meets X )
then A2: ex Y being Subset-Family of T st
( Y c= BB & Y is finite & A = Intersect Y ) by CANTOR_1:def_3;
assume  x in A ; ::_thesis: A meets X
hence  A meets X by A1, A2; ::_thesis: verum
end;
hence  x in Cl X by Th37; ::_thesis: verum
end;

theorem :: YELLOW_9:39
for T being non empty TopSpace
for K being prebasis of T
for x being Point of T
for N being net of T st ( for A being Subset of T st A in K & x in A holds
N is_eventually_in A ) holds
for S being Subset of T st rng (netmap (N,T)) c= S holds
x in Cl S
proof
let T be non empty TopSpace; ::_thesis: for K being prebasis of T
for x being Point of T
for N being net of T st ( for A being Subset of T st A in K & x in A holds
N is_eventually_in A ) holds
for S being Subset of T st rng (netmap (N,T)) c= S holds
x in Cl S
let BB be prebasis of T; ::_thesis: for x being Point of T
for N being net of T st ( for A being Subset of T st A in BB & x in A holds
N is_eventually_in A ) holds
for S being Subset of T st rng (netmap (N,T)) c= S holds
x in Cl S
let x be Point of T; ::_thesis: for N being net of T st ( for A being Subset of T st A in BB & x in A holds
N is_eventually_in A ) holds
for S being Subset of T st rng (netmap (N,T)) c= S holds
x in Cl S
let N be net of T; ::_thesis: ( ( for A being Subset of T st A in BB & x in A holds
N is_eventually_in A ) implies for S being Subset of T st rng (netmap (N,T)) c= S holds
x in Cl S )
assume A1: for A being Subset of T st A in BB & x in A holds
N is_eventually_in A ; ::_thesis: for S being Subset of T st rng (netmap (N,T)) c= S holds
x in Cl S
let S be Subset of T; ::_thesis: ( rng (netmap (N,T)) c= S implies x in Cl S )
assume A2: rng (netmap (N,T)) c= S ; ::_thesis: x in Cl S
A3: [#] N is directed by WAYBEL_0:def_6;
now__::_thesis:_for_Z_being_finite_Subset-Family_of_T_st_Z_c=_BB_&_x_in_Intersect_Z_holds_
Intersect_Z_meets_S
let Z be finite Subset-Family of T; ::_thesis: ( Z c= BB & x in Intersect Z implies Intersect b1 meets S )
assume that
A4: Z c= BB and
A5: x in Intersect Z ; ::_thesis: Intersect b1 meets S
defpred S1[ set , set ] means  for i, j being Element of N st $2 = i & i <= j holds
N . j in $1;
A6: now__::_thesis:_for_a_being_set_st_a_in_Z_holds_
ex_b_being_set_st_
(_b_in_the_carrier_of_N_&_S1[a,b]_)
let a be set ; ::_thesis: ( a in Z implies ex b being set st
( b in the carrier of N & S1[a,b] ) )
assume A7: a in Z ; ::_thesis: ex b being set st
( b in the carrier of N & S1[a,b] )
then reconsider A = a as Subset of T ;
 x in A by A5, A7, SETFAM_1:43;
then  N is_eventually_in A by A1, A4, A7;
then consider i being Element of N such that
A8: for j being Element of N st i <= j holds
N . j in A by WAYBEL_0:def_11;
reconsider b = i as set ;
take b = b; ::_thesis: ( b in the carrier of N & S1[a,b] )
thus  ( b in the carrier of N & S1[a,b] ) by A8; ::_thesis: verum
end;
consider f being Function such that
A9: ( dom f = Z & rng f c= the carrier of N & ( for a being set st a in Z holds
S1[a,f . a] ) ) from FUNCT_1:sch_5(A6);
set k = the Element of N;
percases ( Z = {} or rng f <> {} ) by A9, RELAT_1:42;
suppose Z = {} ; ::_thesis: Intersect b1 meets S
then A10: Intersect Z = the carrier of T by SETFAM_1:def_9;
 N . the Element of N in rng (netmap (N,T)) by FUNCT_2:4;
hence  Intersect Z meets S by A2, A10, XBOOLE_0:3; ::_thesis: verum
end;
suppose rng f <> {} ; ::_thesis: Intersect b1 meets S
then reconsider Y = rng f as non empty finite Subset of N by A9, FINSET_1:8;
consider i being Element of N such that
 i in the carrier of N and
A11: i is_>=_than Y by A3, WAYBEL_0:1;
now__::_thesis:_for_y_being_set_st_y_in_Z_holds_
N_._i_in_y
let y be set ; ::_thesis: ( y in Z implies N . i in y )
assume A12: y in Z ; ::_thesis: N . i in y
then A13: f . y in Y by A9, FUNCT_1:def_3;
then reconsider j = f . y as Element of N ;
 j <= i by A11, A13, LATTICE3:def_9;
hence  N . i in y by A9, A12; ::_thesis: verum
end;
then A14: N . i in Intersect Z by SETFAM_1:43;
 N . i in rng (netmap (N,T)) by FUNCT_2:4;
hence  Intersect Z meets S by A2, A14, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
hence  x in Cl S by Th38; ::_thesis: verum
end;

begin

theorem Th40: :: YELLOW_9:40
for T1, T2 being non empty TopSpace
for B1 being Basis of T1
for B2 being Basis of T2 holds  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  is Basis of [:T1,T2:]
proof
let T1, T2 be non empty TopSpace; ::_thesis: for B1 being Basis of T1
for B2 being Basis of T2 holds  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  is Basis of [:T1,T2:]
let B1 be Basis of T1; ::_thesis: for B2 being Basis of T2 holds  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  is Basis of [:T1,T2:]
let B2 be Basis of T2; ::_thesis:  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  is Basis of [:T1,T2:]
set BB =  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  ;
set T = [:T1,T2:];
A1: the carrier of [:T1,T2:] = [: the carrier of T1, the carrier of T2:] by BORSUK_1:def_2;
  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  c= bool the carrier of [:T1,T2:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  or x in bool the carrier of [:T1,T2:] )
assume  x in  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  ; ::_thesis: x in bool the carrier of [:T1,T2:]
then  ex a being Subset of T1 ex b being Subset of T2 st
( x = [:a,b:] & a in B1 & b in B2 ) ;
hence  x in bool the carrier of [:T1,T2:] ; ::_thesis: verum
end;
then reconsider BB =  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  as Subset-Family of [:T1,T2:] ;
A2: B1 c= the topology of T1 by TOPS_2:64;
A3: B2 c= the topology of T2 by TOPS_2:64;
 BB is Basis of [:T1,T2:]
proof
A4: BB is open
proof
let x be Subset of [:T1,T2:]; :: according to TOPS_2:def_1 ::_thesis: ( not x in BB or x is open )
assume  x in BB ; ::_thesis: x is open
then consider a being Subset of T1, b being Subset of T2 such that
A5: x = [:a,b:] and
A6: a in B1 and
A7: b in B2 ;
A8: a is open by A2, A6, PRE_TOPC:def_2;
 b is open by A3, A7, PRE_TOPC:def_2;
hence  x is open by A5, A8, BORSUK_1:6; ::_thesis: verum
end;
 BB is quasi_basis
proof
let x be set ; :: according to TARSKI:def_3,CANTOR_1:def_2 ::_thesis: ( not x in the topology of [:T1,T2:] or x in UniCl BB )
assume A9: x in the topology of [:T1,T2:] ; ::_thesis: x in UniCl BB
then reconsider X = x as Subset of [:T1,T2:] ;
 X is open by A9, PRE_TOPC:def_2;
then A10: X = union (Base-Appr X) by BORSUK_1:13;
set Y = BB /\ (Base-Appr X);
A11: BB /\ (Base-Appr X) c= BB by XBOOLE_1:17;
reconsider Y = BB /\ (Base-Appr X) as Subset-Family of [:T1,T2:] ;
 union Y = X
proof
thus  union Y c= X by A10, XBOOLE_1:17, ZFMISC_1:77; :: according to XBOOLE_0:def_10 ::_thesis: X c= union Y
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in X or z in union Y )
assume A12: z in X ; ::_thesis: z in union Y
then reconsider p = z as Point of [:T1,T2:] ;
consider z1, z2 being set  such that
A13: z1 in the carrier of T1 and
A14: z2 in the carrier of T2 and
A15: p = [z1,z2] by A1, ZFMISC_1:def_2;
reconsider z1 = z1 as Point of T1 by A13;
reconsider z2 = z2 as Point of T2 by A14;
consider Z being set  such that
A16: z in Z and
A17: Z in Base-Appr X by A10, A12, TARSKI:def_4;
A18: Base-Appr X =  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( [:a,b:] c= X & a is open & b is open )  }  by BORSUK_1:def_3;
then consider a being Subset of T1, b being Subset of T2 such that
A19: Z = [:a,b:] and
A20: [:a,b:] c= X and
A21: a is open and
A22: b is open by A17;
A23: z1 in a by A15, A16, A19, ZFMISC_1:87;
A24: z2 in b by A15, A16, A19, ZFMISC_1:87;
consider a9 being Subset of T1 such that
A25: a9 in B1 and
A26: z1 in a9 and
A27: a9 c= a by A21, A23, Th31;
consider b9 being Subset of T2 such that
A28: b9 in B2 and
A29: z2 in b9 and
A30: b9 c= b by A22, A24, Th31;
 [:a9,b9:] c= [:a,b:] by A27, A30, ZFMISC_1:96;
then A31: [:a9,b9:] c= X by A20, XBOOLE_1:1;
A32: a9 is open by A2, A25, PRE_TOPC:def_2;
 b9 is open by A3, A28, PRE_TOPC:def_2;
then A33: [:a9,b9:] in Base-Appr X by A18, A31, A32;
A34: [:a9,b9:] in BB by A25, A28;
A35: p in [:a9,b9:] by A15, A26, A29, ZFMISC_1:87;
 [:a9,b9:] in Y by A33, A34, XBOOLE_0:def_4;
hence  z in union Y by A35, TARSKI:def_4; ::_thesis: verum
end;
hence  x in UniCl BB by A11, CANTOR_1:def_1; ::_thesis: verum
end;
hence  BB is Basis of [:T1,T2:] by A4; ::_thesis: verum
end;
hence   {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  is Basis of [:T1,T2:] ; ::_thesis: verum
end;

theorem Th41: :: YELLOW_9:41
for T1, T2 being non empty TopSpace
for B1 being prebasis of T1
for B2 being prebasis of T2 holds  {  [: the carrier of T1,b:] where b is Subset of T2 : b in B2  }  \/  {  [:a, the carrier of T2:] where a is Subset of T1 : a in B1  }  is prebasis of [:T1,T2:]
proof
let T1, T2 be non empty TopSpace; ::_thesis: for B1 being prebasis of T1
for B2 being prebasis of T2 holds  {  [: the carrier of T1,b:] where b is Subset of T2 : b in B2  }  \/  {  [:a, the carrier of T2:] where a is Subset of T1 : a in B1  }  is prebasis of [:T1,T2:]
set T = [:T1,T2:];
let B1 be prebasis of T1; ::_thesis: for B2 being prebasis of T2 holds  {  [: the carrier of T1,b:] where b is Subset of T2 : b in B2  }  \/  {  [:a, the carrier of T2:] where a is Subset of T1 : a in B1  }  is prebasis of [:T1,T2:]
let B2 be prebasis of T2; ::_thesis:  {  [: the carrier of T1,b:] where b is Subset of T2 : b in B2  }  \/  {  [:a, the carrier of T2:] where a is Subset of T1 : a in B1  }  is prebasis of [:T1,T2:]
set C2 =  {  [: the carrier of T1,b:] where b is Subset of T2 : b in B2  }  ;
set C1 =  {  [:a, the carrier of T2:] where a is Subset of T1 : a in B1  }  ;
reconsider D1 = FinMeetCl B1 as Basis of T1 by Th23;
reconsider D2 = FinMeetCl B2 as Basis of T2 by Th23;
reconsider D =  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in D1 & b in D2 )  }  as Basis of [:T1,T2:] by Th40;
 the carrier of T1 c= the carrier of T1 ;
then reconsider cT1 = the carrier of T1 as Subset of T1 ;
 the carrier of T2 c= the carrier of T2 ;
then reconsider cT2 = the carrier of T2 as Subset of T2 ;
A1: cT1 in the topology of T1 by PRE_TOPC:def_1;
A2: cT2 in the topology of T2 by PRE_TOPC:def_1;
A3: B1 c= the topology of T1 by TOPS_2:64;
A4: B2 c= the topology of T2 by TOPS_2:64;
  {  [:a, the carrier of T2:] where a is Subset of T1 : a in B1  }  c= bool the carrier of [:T1,T2:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  [:a, the carrier of T2:] where a is Subset of T1 : a in B1  }  or x in bool the carrier of [:T1,T2:] )
assume  x in  {  [:a, the carrier of T2:] where a is Subset of T1 : a in B1  }  ; ::_thesis: x in bool the carrier of [:T1,T2:]
then  ex a being Subset of T1 st
( x = [:a,cT2:] & a in B1 ) ;
hence  x in bool the carrier of [:T1,T2:] ; ::_thesis: verum
end;
then reconsider C1 =  {  [:a, the carrier of T2:] where a is Subset of T1 : a in B1  }  as Subset-Family of [:T1,T2:] ;
reconsider C1 = C1 as Subset-Family of [:T1,T2:] ;
  {  [: the carrier of T1,b:] where b is Subset of T2 : b in B2  }  c= bool the carrier of [:T1,T2:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  [: the carrier of T1,b:] where b is Subset of T2 : b in B2  }  or x in bool the carrier of [:T1,T2:] )
assume  x in  {  [: the carrier of T1,b:] where b is Subset of T2 : b in B2  }  ; ::_thesis: x in bool the carrier of [:T1,T2:]
then  ex a being Subset of T2 st
( x = [:cT1,a:] & a in B2 ) ;
hence  x in bool the carrier of [:T1,T2:] ; ::_thesis: verum
end;
then reconsider C2 =  {  [: the carrier of T1,b:] where b is Subset of T2 : b in B2  }  as Subset-Family of [:T1,T2:] ;
reconsider C2 = C2 as Subset-Family of [:T1,T2:] ;
reconsider C = C2 \/ C1 as Subset-Family of [:T1,T2:] ;
 C is prebasis of [:T1,T2:]
proof
A5: C is open
proof
let x be Subset of [:T1,T2:]; :: according to TOPS_2:def_1 ::_thesis: ( not x in C or x is open )
assume  x in C ; ::_thesis: x is open
then  ( x in C1 or x in C2 ) by XBOOLE_0:def_3;
then  ( ex a being Subset of T1 st
( x = [:a,cT2:] & a in B1 ) or ex a being Subset of T2 st
( x = [:cT1,a:] & a in B2 ) ) ;
then consider a being Subset of T1, b being Subset of T2 such that
A6: x = [:a,b:] and
A7: a in the topology of T1 and
A8: b in the topology of T2 by A1, A2, A3, A4;
A9: a is open by A7, PRE_TOPC:def_2;
 b is open by A8, PRE_TOPC:def_2;
hence  x is open by A6, A9, BORSUK_1:6; ::_thesis: verum
end;
 C is quasi_prebasis
proof
take  D ; :: according to CANTOR_1:def_4 ::_thesis: D c= FinMeetCl C
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in D or d in FinMeetCl C )
assume  d in D ; ::_thesis: d in FinMeetCl C
then consider a being Subset of T1, b being Subset of T2 such that
A10: d = [:a,b:] and
A11: a in D1 and
A12: b in D2 ;
consider aY being Subset-Family of T1 such that
A13: aY c= B1 and
A14: aY is finite and
A15: a = Intersect aY by A11, CANTOR_1:def_3;
consider bY being Subset-Family of T2 such that
A16: bY c= B2 and
A17: bY is finite and
A18: b = Intersect bY by A12, CANTOR_1:def_3;
deffunc H1( Subset of T1) ->  Element of bool the carrier of [:T1,T2:] = [:$1,cT2:];
A19:  {  H1(s) where s is Subset of T1 : s in aY  }  is finite from FRAENKEL:sch_21(A14);
deffunc H2( Subset of T2) ->  Element of bool the carrier of [:T1,T2:] = [:cT1,$1:];
A20:  {  H2(s) where s is Subset of T2 : s in bY  }  is finite from FRAENKEL:sch_21(A17);
set Y1 =  {  [:s,cT2:] where s is Subset of T1 : s in aY  }  ;
set Y2 =  {  [:cT1,s:] where s is Subset of T2 : s in bY  }  ;
A21:  {  [:s,cT2:] where s is Subset of T1 : s in aY  }  c= C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  [:s,cT2:] where s is Subset of T1 : s in aY  }  or x in C )
assume  x in  {  [:s,cT2:] where s is Subset of T1 : s in aY  }  ; ::_thesis: x in C
then  ex s being Subset of T1 st
( x = [:s,cT2:] & s in aY ) ;
then  x in C1 by A13;
hence  x in C by XBOOLE_0:def_3; ::_thesis: verum
end;
A22:  {  [:cT1,s:] where s is Subset of T2 : s in bY  }  c= C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  [:cT1,s:] where s is Subset of T2 : s in bY  }  or x in C )
assume  x in  {  [:cT1,s:] where s is Subset of T2 : s in bY  }  ; ::_thesis: x in C
then  ex s being Subset of T2 st
( x = [:cT1,s:] & s in bY ) ;
then  x in C2 by A16;
hence  x in C by XBOOLE_0:def_3; ::_thesis: verum
end;
set Y =  {  [:s,cT2:] where s is Subset of T1 : s in aY  }  \/  {  [:cT1,s:] where s is Subset of T2 : s in bY  }  ;
A23:  {  [:s,cT2:] where s is Subset of T1 : s in aY  }  \/  {  [:cT1,s:] where s is Subset of T2 : s in bY  }  c= C by A21, A22, XBOOLE_1:8;
then reconsider Y =  {  [:s,cT2:] where s is Subset of T1 : s in aY  }  \/  {  [:cT1,s:] where s is Subset of T2 : s in bY  }  as Subset-Family of [:T1,T2:] by XBOOLE_1:1;
 Intersect Y = d
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: d c= Intersect Y
let p be set ; ::_thesis: ( p in Intersect Y implies p in d )
assume A24: p in Intersect Y ; ::_thesis: p in d
then consider p1 being Point of T1, p2 being Point of T2 such that
A25: p = [p1,p2] by BORSUK_1:10;
now__::_thesis:_for_z_being_set_st_z_in_aY_holds_
p1_in_z
let z be set ; ::_thesis: ( z in aY implies p1 in z )
assume A26: z in aY ; ::_thesis: p1 in z
then reconsider z9 = z as Subset of T1 ;
 [:z9,cT2:] in  {  [:s,cT2:] where s is Subset of T1 : s in aY  }  by A26;
then  [:z9,cT2:] in Y by XBOOLE_0:def_3;
then  p in [:z9,cT2:] by A24, SETFAM_1:43;
hence  p1 in z by A25, ZFMISC_1:87; ::_thesis: verum
end;
then A27: p1 in a by A15, SETFAM_1:43;
now__::_thesis:_for_z_being_set_st_z_in_bY_holds_
p2_in_z
let z be set ; ::_thesis: ( z in bY implies p2 in z )
assume A28: z in bY ; ::_thesis: p2 in z
then reconsider z9 = z as Subset of T2 ;
 [:cT1,z9:] in  {  [:cT1,s:] where s is Subset of T2 : s in bY  }  by A28;
then  [:cT1,z9:] in Y by XBOOLE_0:def_3;
then  p in [:cT1,z9:] by A24, SETFAM_1:43;
hence  p2 in z by A25, ZFMISC_1:87; ::_thesis: verum
end;
then  p2 in b by A18, SETFAM_1:43;
hence  p in d by A10, A25, A27, ZFMISC_1:87; ::_thesis: verum
end;
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in d or p in Intersect Y )
assume  p in d ; ::_thesis: p in Intersect Y
then consider p1, p2 being set  such that
A29: p1 in a and
A30: p2 in b and
A31: [p1,p2] = p by A10, ZFMISC_1:def_2;
reconsider p1 = p1 as Point of T1 by A29;
reconsider p2 = p2 as Point of T2 by A30;
now__::_thesis:_for_z_being_set_st_z_in_Y_holds_
[p1,p2]_in_z
let z be set ; ::_thesis: ( z in Y implies [p1,p2] in b1 )
assume A32: z in Y ; ::_thesis: [p1,p2] in b1
percases ( z in  {  [:s,cT2:] where s is Subset of T1 : s in aY  }  or z in  {  [:cT1,s:] where s is Subset of T2 : s in bY  }  ) by A32, XBOOLE_0:def_3;
suppose z in  {  [:s,cT2:] where s is Subset of T1 : s in aY  }  ; ::_thesis: [p1,p2] in b1
then consider s being Subset of T1 such that
A33: z = [:s,cT2:] and
A34: s in aY ;
 p1 in s by A15, A29, A34, SETFAM_1:43;
hence  [p1,p2] in z by A33, ZFMISC_1:87; ::_thesis: verum
end;
suppose z in  {  [:cT1,s:] where s is Subset of T2 : s in bY  }  ; ::_thesis: [p1,p2] in b1
then consider s being Subset of T2 such that
A35: z = [:cT1,s:] and
A36: s in bY ;
 p2 in s by A18, A30, A36, SETFAM_1:43;
hence  [p1,p2] in z by A35, ZFMISC_1:87; ::_thesis: verum
end;
end;
end;
hence  p in Intersect Y by A31, SETFAM_1:43; ::_thesis: verum
end;
hence  d in FinMeetCl C by A19, A20, A23, CANTOR_1:def_3; ::_thesis: verum
end;
hence  C is prebasis of [:T1,T2:] by A5; ::_thesis: verum
end;
hence   {  [: the carrier of T1,b:] where b is Subset of T2 : b in B2  }  \/  {  [:a, the carrier of T2:] where a is Subset of T1 : a in B1  }  is prebasis of [:T1,T2:] ; ::_thesis: verum
end;

theorem :: YELLOW_9:42
for X1, X2 being set
for A being Subset-Family of [:X1,X2:]
for A1 being non empty Subset-Family of X1
for A2 being non empty Subset-Family of X2 st A =  {  [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 )  }  holds
Intersect A = [:(Intersect A1),(Intersect A2):]
proof
let X1, X2 be set ; ::_thesis: for A being Subset-Family of [:X1,X2:]
for A1 being non empty Subset-Family of X1
for A2 being non empty Subset-Family of X2 st A =  {  [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 )  }  holds
Intersect A = [:(Intersect A1),(Intersect A2):]
let A be Subset-Family of [:X1,X2:]; ::_thesis: for A1 being non empty Subset-Family of X1
for A2 being non empty Subset-Family of X2 st A =  {  [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 )  }  holds
Intersect A = [:(Intersect A1),(Intersect A2):]
let A1 be non empty Subset-Family of X1; ::_thesis: for A2 being non empty Subset-Family of X2 st A =  {  [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 )  }  holds
Intersect A = [:(Intersect A1),(Intersect A2):]
let A2 be non empty Subset-Family of X2; ::_thesis: ( A =  {  [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 )  }  implies Intersect A = [:(Intersect A1),(Intersect A2):] )
assume A1: A =  {  [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 )  }  ; ::_thesis: Intersect A = [:(Intersect A1),(Intersect A2):]
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: [:(Intersect A1),(Intersect A2):] c= Intersect A
let x be set ; ::_thesis: ( x in Intersect A implies x in [:(Intersect A1),(Intersect A2):] )
assume A2: x in Intersect A ; ::_thesis: x in [:(Intersect A1),(Intersect A2):]
then consider x1, x2 being set  such that
A3: x1 in X1 and
A4: x2 in X2 and
A5: [x1,x2] = x by ZFMISC_1:def_2;
set a1 = the Element of A1;
set a2 = the Element of A2;
reconsider a1 = the Element of A1 as Subset of X1 ;
reconsider a2 = the Element of A2 as Subset of X2 ;
now__::_thesis:_for_a_being_set_st_a_in_A1_holds_
x1_in_a
let a be set ; ::_thesis: ( a in A1 implies x1 in a )
assume  a in A1 ; ::_thesis: x1 in a
then  [:a,a2:] in A by A1;
then  x in [:a,a2:] by A2, SETFAM_1:43;
hence  x1 in a by A5, ZFMISC_1:87; ::_thesis: verum
end;
then A6: x1 in Intersect A1 by A3, SETFAM_1:43;
now__::_thesis:_for_a_being_set_st_a_in_A2_holds_
x2_in_a
let a be set ; ::_thesis: ( a in A2 implies x2 in a )
assume  a in A2 ; ::_thesis: x2 in a
then  [:a1,a:] in A by A1;
then  x in [:a1,a:] by A2, SETFAM_1:43;
hence  x2 in a by A5, ZFMISC_1:87; ::_thesis: verum
end;
then  x2 in Intersect A2 by A4, SETFAM_1:43;
hence  x in [:(Intersect A1),(Intersect A2):] by A5, A6, ZFMISC_1:87; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:(Intersect A1),(Intersect A2):] or x in Intersect A )
assume A7: x in [:(Intersect A1),(Intersect A2):] ; ::_thesis: x in Intersect A
then consider x1, x2 being set  such that
A8: x1 in Intersect A1 and
A9: x2 in Intersect A2 and
A10: [x1,x2] = x by ZFMISC_1:def_2;
now__::_thesis:_for_c_being_set_st_c_in_A_holds_
x_in_c
let c be set ; ::_thesis: ( c in A implies x in c )
assume  c in A ; ::_thesis: x in c
then consider a being Subset of X1, b being Subset of X2 such that
A11: c = [:a,b:] and
A12: a in A1 and
A13: b in A2 by A1;
A14: x1 in a by A8, A12, SETFAM_1:43;
 x2 in b by A9, A13, SETFAM_1:43;
hence  x in c by A10, A11, A14, ZFMISC_1:87; ::_thesis: verum
end;
hence  x in Intersect A by A7, SETFAM_1:43; ::_thesis: verum
end;

theorem :: YELLOW_9:43
for T1, T2 being non empty TopSpace
for B1 being prebasis of T1
for B2 being prebasis of T2 st union B1 = the carrier of T1 & union B2 = the carrier of T2 holds
{  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  is prebasis of [:T1,T2:]
proof
let T1, T2 be non empty TopSpace; ::_thesis: for B1 being prebasis of T1
for B2 being prebasis of T2 st union B1 = the carrier of T1 & union B2 = the carrier of T2 holds
{  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  is prebasis of [:T1,T2:]
let B1 be prebasis of T1; ::_thesis: for B2 being prebasis of T2 st union B1 = the carrier of T1 & union B2 = the carrier of T2 holds
{  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  is prebasis of [:T1,T2:]
let B2 be prebasis of T2; ::_thesis: ( union B1 = the carrier of T1 & union B2 = the carrier of T2 implies  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  is prebasis of [:T1,T2:] )
assume that
A1: union B1 = the carrier of T1 and
A2: union B2 = the carrier of T2 ; ::_thesis:  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  is prebasis of [:T1,T2:]
set cT1 = the carrier of T1;
set cT2 = the carrier of T2;
set BB1 =  {  [: the carrier of T1,b:] where b is Subset of T2 : b in B2  }  ;
set BB2 =  {  [:a, the carrier of T2:] where a is Subset of T1 : a in B1  }  ;
set CC =  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  ;
set T = [:T1,T2:];
reconsider BB =  {  [: the carrier of T1,b:] where b is Subset of T2 : b in B2  }  \/  {  [:a, the carrier of T2:] where a is Subset of T1 : a in B1  }  as prebasis of [:T1,T2:] by Th41;
A3: FinMeetCl BB is Basis of [:T1,T2:] by Th23;
  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  c= bool the carrier of [:T1,T2:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  or x in bool the carrier of [:T1,T2:] )
assume  x in  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  ; ::_thesis: x in bool the carrier of [:T1,T2:]
then  ex a being Subset of T1 ex b being Subset of T2 st
( x = [:a,b:] & a in B1 & b in B2 ) ;
hence  x in bool the carrier of [:T1,T2:] ; ::_thesis: verum
end;
then reconsider CC =  {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  as Subset-Family of [:T1,T2:] ;
reconsider CC = CC as Subset-Family of [:T1,T2:] ;
 CC c= the topology of [:T1,T2:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in CC or x in the topology of [:T1,T2:] )
assume  x in CC ; ::_thesis: x in the topology of [:T1,T2:]
then consider a being Subset of T1, b being Subset of T2 such that
A4: x = [:a,b:] and
A5: a in B1 and
A6: b in B2 ;
A7: B1 c= the topology of T1 by TOPS_2:64;
A8: B2 c= the topology of T2 by TOPS_2:64;
A9: a is open by A5, A7, PRE_TOPC:def_2;
 b is open by A6, A8, PRE_TOPC:def_2;
then  [:a,b:] is open by A9, BORSUK_1:6;
hence  x in the topology of [:T1,T2:] by A4, PRE_TOPC:def_2; ::_thesis: verum
end;
then  UniCl CC c= UniCl the topology of [:T1,T2:] by CANTOR_1:9;
then A10: UniCl CC c= the topology of [:T1,T2:] by CANTOR_1:6;
 BB c= UniCl CC
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in BB or x in UniCl CC )
assume A11: x in BB ; ::_thesis: x in UniCl CC
percases ( x in  {  [: the carrier of T1,b:] where b is Subset of T2 : b in B2  }  or x in  {  [:a, the carrier of T2:] where a is Subset of T1 : a in B1  }  ) by A11, XBOOLE_0:def_3;
suppose x in  {  [: the carrier of T1,b:] where b is Subset of T2 : b in B2  }  ; ::_thesis: x in UniCl CC
then consider b being Subset of T2 such that
A12: x = [: the carrier of T1,b:] and
A13: b in B2 ;
set Y =  {  [:a,b:] where a is Subset of T1 : a in B1  }  ;
  {  [:a,b:] where a is Subset of T1 : a in B1  }  c= bool the carrier of [:T1,T2:]
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  [:a,b:] where a is Subset of T1 : a in B1  }  or y in bool the carrier of [:T1,T2:] )
assume  y in  {  [:a,b:] where a is Subset of T1 : a in B1  }  ; ::_thesis: y in bool the carrier of [:T1,T2:]
then  ex a being Subset of T1 st
( y = [:a,b:] & a in B1 ) ;
hence  y in bool the carrier of [:T1,T2:] ; ::_thesis: verum
end;
then reconsider Y =  {  [:a,b:] where a is Subset of T1 : a in B1  }  as Subset-Family of [:T1,T2:] ;
reconsider Y = Y as Subset-Family of [:T1,T2:] ;
A14: Y c= CC
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in CC )
assume  y in Y ; ::_thesis: y in CC
then  ex a being Subset of T1 st
( y = [:a,b:] & a in B1 ) ;
hence  y in CC by A13; ::_thesis: verum
end;
 x = union Y
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: union Y c= x
let z be set ; ::_thesis: ( z in x implies z in union Y )
assume  z in x ; ::_thesis: z in union Y
then consider p1, p2 being set  such that
A15: p1 in the carrier of T1 and
A16: p2 in b and
A17: [p1,p2] = z by A12, ZFMISC_1:def_2;
consider a being set  such that
A18: p1 in a and
A19: a in B1 by A1, A15, TARSKI:def_4;
reconsider a = a as Subset of T1 by A19;
A20: [:a,b:] in Y by A19;
 z in [:a,b:] by A16, A17, A18, ZFMISC_1:def_2;
hence  z in union Y by A20, TARSKI:def_4; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union Y or z in x )
assume  z in union Y ; ::_thesis: z in x
then consider y being set  such that
A21: z in y and
A22: y in Y by TARSKI:def_4;
 ex a being Subset of T1 st
( y = [:a,b:] & a in B1 ) by A22;
then  y c= x by A12, ZFMISC_1:95;
hence  z in x by A21; ::_thesis: verum
end;
hence  x in UniCl CC by A14, CANTOR_1:def_1; ::_thesis: verum
end;
suppose x in  {  [:a, the carrier of T2:] where a is Subset of T1 : a in B1  }  ; ::_thesis: x in UniCl CC
then consider a being Subset of T1 such that
A23: x = [:a, the carrier of T2:] and
A24: a in B1 ;
set Y =  {  [:a,b:] where b is Subset of T2 : b in B2  }  ;
  {  [:a,b:] where b is Subset of T2 : b in B2  }  c= bool the carrier of [:T1,T2:]
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  [:a,b:] where b is Subset of T2 : b in B2  }  or y in bool the carrier of [:T1,T2:] )
assume  y in  {  [:a,b:] where b is Subset of T2 : b in B2  }  ; ::_thesis: y in bool the carrier of [:T1,T2:]
then  ex b being Subset of T2 st
( y = [:a,b:] & b in B2 ) ;
hence  y in bool the carrier of [:T1,T2:] ; ::_thesis: verum
end;
then reconsider Y =  {  [:a,b:] where b is Subset of T2 : b in B2  }  as Subset-Family of [:T1,T2:] ;
reconsider Y = Y as Subset-Family of [:T1,T2:] ;
A25: Y c= CC
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in CC )
assume  y in Y ; ::_thesis: y in CC
then  ex b being Subset of T2 st
( y = [:a,b:] & b in B2 ) ;
hence  y in CC by A24; ::_thesis: verum
end;
 x = union Y
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: union Y c= x
let z be set ; ::_thesis: ( z in x implies z in union Y )
assume  z in x ; ::_thesis: z in union Y
then consider p1, p2 being set  such that
A26: p1 in a and
A27: p2 in the carrier of T2 and
A28: [p1,p2] = z by A23, ZFMISC_1:def_2;
consider b being set  such that
A29: p2 in b and
A30: b in B2 by A2, A27, TARSKI:def_4;
reconsider b = b as Subset of T2 by A30;
A31: [:a,b:] in Y by A30;
 z in [:a,b:] by A26, A28, A29, ZFMISC_1:def_2;
hence  z in union Y by A31, TARSKI:def_4; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union Y or z in x )
assume  z in union Y ; ::_thesis: z in x
then consider y being set  such that
A32: z in y and
A33: y in Y by TARSKI:def_4;
 ex b being Subset of T2 st
( y = [:a,b:] & b in B2 ) by A33;
then  y c= x by A23, ZFMISC_1:95;
hence  z in x by A32; ::_thesis: verum
end;
hence  x in UniCl CC by A25, CANTOR_1:def_1; ::_thesis: verum
end;
end;
end;
then  FinMeetCl BB c= FinMeetCl (UniCl CC) by CANTOR_1:14;
then  UniCl CC is prebasis of [:T1,T2:] by A3, A10, CANTOR_1:def_4, TOPS_2:64;
hence   {  [:a,b:] where a is Subset of T1, b is Subset of T2 : ( a in B1 & b in B2 )  }  is prebasis of [:T1,T2:] by Th24; ::_thesis: verum
end;

begin

definition
let R be RelStr ;
mode TopAugmentation of R ->  TopRelStr  means :Def4: :: YELLOW_9:def 4
 RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of R, the InternalRel of R #);
existence
 ex b1 being TopRelStr st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #)
proof
take  TopRelStr(# the carrier of R, the InternalRel of R,({} (bool the carrier of R)) #) ; ::_thesis: RelStr(# the carrier of TopRelStr(# the carrier of R, the InternalRel of R,({} (bool the carrier of R)) #), the InternalRel of TopRelStr(# the carrier of R, the InternalRel of R,({} (bool the carrier of R)) #) #) = RelStr(# the carrier of R, the InternalRel of R #)
thus  RelStr(# the carrier of TopRelStr(# the carrier of R, the InternalRel of R,({} (bool the carrier of R)) #), the InternalRel of TopRelStr(# the carrier of R, the InternalRel of R,({} (bool the carrier of R)) #) #) = RelStr(# the carrier of R, the InternalRel of R #) ; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines TopAugmentation YELLOW_9:def_4_:_
 for R being RelStr
for b2 being TopRelStr holds
( b2 is TopAugmentation of R iff RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of R, the InternalRel of R #) );

notation
let R be RelStr ;
let T be TopAugmentation of R;
synonym  correct T for  TopSpace-like ;
end;

registration
let R be RelStr ;
cluster correct discrete strict for TopAugmentation of R;
existence
 ex b1 being TopAugmentation of R st
( b1 is correct & b1 is discrete & b1 is strict )
proof
reconsider BB = bool the carrier of R as Subset-Family of R ;
set T = TopRelStr(# the carrier of R, the InternalRel of R,BB #);
 RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of TopRelStr(# the carrier of R, the InternalRel of R,BB #), the InternalRel of TopRelStr(# the carrier of R, the InternalRel of R,BB #) #) ;
then reconsider T = TopRelStr(# the carrier of R, the InternalRel of R,BB #) as TopAugmentation of R by Def4;
take  T ; ::_thesis: ( T is correct & T is discrete & T is strict )
 T is discrete TopStruct by TDLAT_3:def_1;
hence  ( T is correct & T is discrete & T is strict ) ; ::_thesis: verum
end;
end;

theorem :: YELLOW_9:44
for T being TopRelStr holds T is TopAugmentation of T
proof
let T be TopRelStr ; ::_thesis: T is TopAugmentation of T
thus  RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T, the InternalRel of T #) ; :: according to YELLOW_9:def_4 ::_thesis: verum
end;

theorem :: YELLOW_9:45
for S being TopRelStr
for T being TopAugmentation of S holds S is TopAugmentation of T
proof
let S be TopRelStr ; ::_thesis: for T being TopAugmentation of S holds S is TopAugmentation of T
let T be TopAugmentation of S; ::_thesis: S is TopAugmentation of T
thus  RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) by Def4; :: according to YELLOW_9:def_4 ::_thesis: verum
end;

theorem :: YELLOW_9:46
for R being RelStr
for T1 being TopAugmentation of R
for T2 being TopAugmentation of T1 holds T2 is TopAugmentation of R
proof
let R be RelStr ; ::_thesis: for T1 being TopAugmentation of R
for T2 being TopAugmentation of T1 holds T2 is TopAugmentation of R
let T1 be TopAugmentation of R; ::_thesis: for T2 being TopAugmentation of T1 holds T2 is TopAugmentation of R
let T2 be TopAugmentation of T1; ::_thesis: T2 is TopAugmentation of R
thus  RelStr(# the carrier of T2, the InternalRel of T2 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) by Def4
.= RelStr(# the carrier of R, the InternalRel of R #) by Def4 ; :: according to YELLOW_9:def_4 ::_thesis: verum
end;

registration
let R be non empty RelStr ;
cluster  ->  non empty for TopAugmentation of R;
coherence
 for b1 being TopAugmentation of R holds not b1 is empty
proof
let T be TopAugmentation of R; ::_thesis: not T is empty
 RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by Def4;
hence  not the carrier of T is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

registration
let R be reflexive RelStr ;
cluster  ->  reflexive for TopAugmentation of R;
coherence
 for b1 being TopAugmentation of R holds b1 is reflexive
proof
let T be TopAugmentation of R; ::_thesis: T is reflexive
 RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by Def4;
hence  the InternalRel of T is_reflexive_in the carrier of T by ORDERS_2:def_2; :: according to ORDERS_2:def_2 ::_thesis: verum
end;
end;

registration
let R be transitive RelStr ;
cluster  ->  transitive for TopAugmentation of R;
coherence
 for b1 being TopAugmentation of R holds b1 is transitive
proof
let T be TopAugmentation of R; ::_thesis: T is transitive
 RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by Def4;
then  the InternalRel of T is_transitive_in the carrier of T by ORDERS_2:def_3;
hence  T is transitive by ORDERS_2:def_3; ::_thesis: verum
end;
end;

registration
let R be antisymmetric RelStr ;
cluster  ->  antisymmetric for TopAugmentation of R;
coherence
 for b1 being TopAugmentation of R holds b1 is antisymmetric
proof
let T be TopAugmentation of R; ::_thesis: T is antisymmetric
 RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by Def4;
then  the InternalRel of T is_antisymmetric_in the carrier of T by ORDERS_2:def_4;
hence  T is antisymmetric by ORDERS_2:def_4; ::_thesis: verum
end;
end;

registration
let R be non empty complete RelStr ;
cluster  ->  complete for TopAugmentation of R;
coherence
 for b1 being TopAugmentation of R holds b1 is complete
proof
let T be TopAugmentation of R; ::_thesis: T is complete
 RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by Def4;
hence  T is complete by YELLOW_0:3; ::_thesis: verum
end;
end;

theorem Th47: :: YELLOW_9:47
for S being non empty reflexive antisymmetric up-complete RelStr
for T being non empty reflexive RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds
for A being Subset of S
for C being Subset of T st A = C & A is inaccessible holds
C is inaccessible
proof
let S be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for T being non empty reflexive RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds
for A being Subset of S
for C being Subset of T st A = C & A is inaccessible holds
C is inaccessible
let T be non empty reflexive RelStr ; ::_thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) implies for A being Subset of S
for C being Subset of T st A = C & A is inaccessible holds
C is inaccessible )
assume A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) ; ::_thesis: for A being Subset of S
for C being Subset of T st A = C & A is inaccessible holds
C is inaccessible
let A be Subset of S; ::_thesis: for C being Subset of T st A = C & A is inaccessible holds
C is inaccessible
let C be Subset of T; ::_thesis: ( A = C & A is inaccessible implies C is inaccessible )
assume that
A2: A = C and
A3: for D being non empty directed Subset of S st sup D in A holds
D meets A ; :: according to WAYBEL11:def_1 ::_thesis: C is inaccessible
let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( not sup D in C or not D misses C )
assume A4: sup D in C ; ::_thesis: not D misses C
reconsider E = D as non empty directed Subset of S by A1, WAYBEL_0:3;
 ex_sup_of E,S by WAYBEL_0:75;
then  sup D = sup E by A1, YELLOW_0:26;
hence  not D misses C by A2, A3, A4; ::_thesis: verum
end;

theorem Th48: :: YELLOW_9:48
for S being non empty reflexive RelStr
for T being TopAugmentation of S st the topology of T = sigma S holds
T is correct
proof
let R be non empty reflexive RelStr ; ::_thesis: for T being TopAugmentation of R st the topology of T = sigma R holds
T is correct
let T be TopAugmentation of R; ::_thesis: ( the topology of T = sigma R implies T is correct )
assume A1: the topology of T = sigma R ; ::_thesis: T is correct
A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by Def4;
set IT = ConvergenceSpace (Scott-Convergence R);
A3: the carrier of (ConvergenceSpace (Scott-Convergence R)) = the carrier of R by YELLOW_6:def_24;
then A4: the carrier of T in sigma R by A2, PRE_TOPC:def_1;
A5: for a being Subset-Family of T st a c= the topology of T holds
union a in the topology of T by A1, A2, A3, PRE_TOPC:def_1;
 for a, b being Subset of T st a in the topology of T & b in the topology of T holds
a /\ b in the topology of T by A1, PRE_TOPC:def_1;
hence  T is correct by A1, A4, A5, PRE_TOPC:def_1; ::_thesis: verum
end;

theorem Th49: :: YELLOW_9:49
for S being complete LATTICE
for T being TopAugmentation of S st the topology of T = sigma S holds
T is Scott
proof
let R be complete LATTICE; ::_thesis: for T being TopAugmentation of R st the topology of T = sigma R holds
T is Scott
let T be TopAugmentation of R; ::_thesis: ( the topology of T = sigma R implies T is Scott )
assume A1: the topology of T = sigma R ; ::_thesis: T is Scott
A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by Def4;
 T is Scott
proof
let S be Subset of T; :: according to WAYBEL11:def_4 ::_thesis: ( ( not S is open or ( S is inaccessible_by_directed_joins & S is upper ) ) & ( not S is inaccessible_by_directed_joins or not S is upper or S is open ) )
reconsider A = S as Subset of R by A2;
thus  ( S is open implies ( S is inaccessible & S is upper ) ) ::_thesis: ( not S is inaccessible_by_directed_joins or not S is upper or S is open )
proof
assume  S in the topology of T ; :: according to PRE_TOPC:def_2 ::_thesis: ( S is inaccessible & S is upper )
then  ( A is inaccessible & A is upper ) by A1, WAYBEL11:31;
hence  ( S is inaccessible & S is upper ) by A2, Th47, WAYBEL_0:25; ::_thesis: verum
end;
assume  ( S is inaccessible & S is upper ) ; ::_thesis: S is open
then  ( A is inaccessible & A is upper ) by A2, Th47, WAYBEL_0:25;
hence  S in the topology of T by A1, WAYBEL11:31; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
hence  T is Scott ; ::_thesis: verum
end;

registration
let R be complete LATTICE;
cluster non empty correct reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V194() up-complete /\-complete strict Scott for TopAugmentation of R;
existence
 ex b1 being TopAugmentation of R st
( b1 is Scott & b1 is strict & b1 is correct )
proof
set T = TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #);
 RelStr(# the carrier of TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #), the InternalRel of TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #) #) = RelStr(# the carrier of R, the InternalRel of R #) ;
then reconsider T = TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #) as TopAugmentation of R by Def4;
take  T ; ::_thesis: ( T is Scott & T is strict & T is correct )
thus  ( T is Scott & T is strict & T is correct ) by Th48, Th49; ::_thesis: verum
end;
end;

theorem Th50: :: YELLOW_9:50
for S, T being non empty reflexive transitive antisymmetric complete Scott TopRelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds
for F being Subset of S
for G being Subset of T st F = G & F is open holds
G is open
proof
let S, T be non empty reflexive transitive antisymmetric complete Scott TopRelStr ; ::_thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) implies for F being Subset of S
for G being Subset of T st F = G & F is open holds
G is open )
assume A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) ; ::_thesis: for F being Subset of S
for G being Subset of T st F = G & F is open holds
G is open
let F be Subset of S; ::_thesis: for G being Subset of T st F = G & F is open holds
G is open
let G be Subset of T; ::_thesis: ( F = G & F is open implies G is open )
assume that
A2: F = G and
A3: F is open ; ::_thesis: G is open
 ( F is upper & F is inaccessible ) by A3, WAYBEL11:def_4;
then  ( G is upper & G is inaccessible ) by A1, A2, Th47, WAYBEL_0:25;
hence  G is open by WAYBEL11:def_4; ::_thesis: verum
end;

theorem Th51: :: YELLOW_9:51
for S being complete LATTICE
for T being Scott TopAugmentation of S holds the topology of T = sigma S
proof
let S be complete LATTICE; ::_thesis: for T being Scott TopAugmentation of S holds the topology of T = sigma S
let T be Scott TopAugmentation of S; ::_thesis: the topology of T = sigma S
set R = TopRelStr(# the carrier of S, the InternalRel of S,(sigma S) #);
 RelStr(# the carrier of TopRelStr(# the carrier of S, the InternalRel of S,(sigma S) #), the InternalRel of TopRelStr(# the carrier of S, the InternalRel of S,(sigma S) #) #) = RelStr(# the carrier of S, the InternalRel of S #) ;
then reconsider R = TopRelStr(# the carrier of S, the InternalRel of S,(sigma S) #) as TopAugmentation of S by Def4;
reconsider R = R as correct Scott TopAugmentation of S by Th48, Th49;
A1: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by Def4;
thus  the topology of T c= sigma S :: according to XBOOLE_0:def_10 ::_thesis: sigma S c= the topology of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of T or x in sigma S )
assume A2: x in the topology of T ; ::_thesis: x in sigma S
then reconsider A = x as Subset of T ;
reconsider C = A as Subset of R by A1;
 A is open by A2, PRE_TOPC:def_2;
then  C is open by A1, Th50;
hence  x in sigma S by PRE_TOPC:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in sigma S or x in the topology of T )
assume A3: x in sigma S ; ::_thesis: x in the topology of T
then reconsider A = x as Subset of R ;
reconsider C = A as Subset of T by A1;
 A is open by A3, PRE_TOPC:def_2;
then  C is open by A1, Th50;
hence  x in the topology of T by PRE_TOPC:def_2; ::_thesis: verum
end;

theorem :: YELLOW_9:52
for S, T being complete LATTICE st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds
sigma S = sigma T
proof
let S, T be complete LATTICE; ::_thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) implies sigma S = sigma T )
assume A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) ; ::_thesis: sigma S = sigma T
set A = the correct Scott TopAugmentation of S;
 RelStr(# the carrier of the correct Scott TopAugmentation of S, the InternalRel of the correct Scott TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #) by Def4;
then  the correct Scott TopAugmentation of S is correct Scott TopAugmentation of T by A1, Def4;
then  the topology of the correct Scott TopAugmentation of S = sigma T by Th51;
hence  sigma S = sigma T by Th51; ::_thesis: verum
end;

registration
let R be complete LATTICE;
cluster Scott  ->  correct for TopAugmentation of R;
coherence
 for b1 being TopAugmentation of R st b1 is Scott holds
b1 is correct
proof
let T be TopAugmentation of R; ::_thesis: ( T is Scott implies T is correct )
assume  T is Scott ; ::_thesis: T is correct
then  the topology of T = sigma R by Th51;
hence  T is correct by Th48; ::_thesis: verum
end;
end;

Lm1:  for S being TopStruct ex T being strict TopSpace st
( the carrier of T = the carrier of S & the topology of S is prebasis of T )
proof
let S be TopStruct ; ::_thesis: ex T being strict TopSpace st
( the carrier of T = the carrier of S & the topology of S is prebasis of T )
set T = TopStruct(# the carrier of S,(UniCl (FinMeetCl the topology of S)) #);
A1: {{},{}} = {{}} by ENUMSET1:29;
now__::_thesis:_(_the_carrier_of_S_=_{}_implies_TopStruct(#_the_carrier_of_S,(UniCl_(FinMeetCl_the_topology_of_S))_#)_is_discrete_TopStruct_)
assume A2: the carrier of S = {} ; ::_thesis: TopStruct(# the carrier of S,(UniCl (FinMeetCl the topology of S)) #) is discrete TopStruct
then  ( the topology of S = {} or the topology of S = {{}} ) by ZFMISC_1:1, ZFMISC_1:33;
then  FinMeetCl the topology of S = {{}} by A1, A2, Th11, Th17;
then  UniCl (FinMeetCl the topology of S) = {{}} by A1, Th11;
hence  TopStruct(# the carrier of S,(UniCl (FinMeetCl the topology of S)) #) is discrete TopStruct by A2, TDLAT_3:def_1, ZFMISC_1:1; ::_thesis: verum
end;
then reconsider T = TopStruct(# the carrier of S,(UniCl (FinMeetCl the topology of S)) #) as strict TopSpace by CANTOR_1:15;
take  T ; ::_thesis: ( the carrier of T = the carrier of S & the topology of S is prebasis of T )
A3: the topology of S c= FinMeetCl the topology of S by CANTOR_1:4;
 FinMeetCl the topology of S c= the topology of T by CANTOR_1:1;
then A4: the topology of S c= the topology of T by A3, XBOOLE_1:1;
 FinMeetCl the topology of S is Basis of T by Th22;
hence  ( the carrier of T = the carrier of S & the topology of S is prebasis of T ) by A4, CANTOR_1:def_4, TOPS_2:64; ::_thesis: verum
end;

begin

definition
let T be TopStruct ;
mode TopExtension of T ->  TopSpace means :Def5: :: YELLOW_9:def 5
( the carrier of T = the carrier of it & the topology of T c= the topology of it );
existence
 ex b1 being TopSpace st
( the carrier of T = the carrier of b1 & the topology of T c= the topology of b1 )
proof
consider R being strict TopSpace such that
A1: the carrier of R = the carrier of T and
A2: the topology of T is prebasis of R by Lm1;
take  R ; ::_thesis: ( the carrier of T = the carrier of R & the topology of T c= the topology of R )
thus  ( the carrier of T = the carrier of R & the topology of T c= the topology of R ) by A1, A2, TOPS_2:64; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines TopExtension YELLOW_9:def_5_:_
 for T being TopStruct
for b2 being TopSpace holds
( b2 is TopExtension of T iff ( the carrier of T = the carrier of b2 & the topology of T c= the topology of b2 ) );

theorem Th53: :: YELLOW_9:53
for S being TopStruct ex T being TopExtension of S st
( T is strict & the topology of S is prebasis of T )
proof
let S be TopStruct ; ::_thesis: ex T being TopExtension of S st
( T is strict & the topology of S is prebasis of T )
consider T being strict TopSpace such that
A1: the carrier of T = the carrier of S and
A2: the topology of S is prebasis of T by Lm1;
 the topology of S c= the topology of T by A2, TOPS_2:64;
then reconsider T = T as TopExtension of S by A1, Def5;
take  T ; ::_thesis: ( T is strict & the topology of S is prebasis of T )
thus  ( T is strict & the topology of S is prebasis of T ) by A2; ::_thesis: verum
end;

registration
let T be TopStruct ;
cluster strict correct discrete for TopExtension of T;
existence
 ex b1 being TopExtension of T st
( b1 is strict & b1 is discrete )
proof
reconsider S = bool the carrier of T as Subset-Family of T ;
reconsider S = S as Subset-Family of T ;
set R = TopStruct(# the carrier of T,S #);
A1: TopStruct(# the carrier of T,S #) is discrete TopStruct by TDLAT_3:def_1;
 the topology of T c= S ;
then  TopStruct(# the carrier of T,S #) is TopExtension of T by A1, Def5;
hence  ex b1 being TopExtension of T st
( b1 is strict & b1 is discrete ) by A1; ::_thesis: verum
end;
end;

definition
let T1, T2 be TopStruct ;
mode Refinement of T1,T2 ->  TopSpace means :Def6: :: YELLOW_9:def 6
( the carrier of it = the carrier of T1 \/ the carrier of T2 & the topology of T1 \/ the topology of T2 is prebasis of it );
existence
 ex b1 being TopSpace st
( the carrier of b1 = the carrier of T1 \/ the carrier of T2 & the topology of T1 \/ the topology of T2 is prebasis of b1 )
proof
set c1 = the carrier of T1;
set c2 = the carrier of T2;
set t1 = the topology of T1;
set t2 = the topology of T2;
A1: bool the carrier of T1 c= bool ( the carrier of T1 \/ the carrier of T2) by XBOOLE_1:7, ZFMISC_1:67;
A2: bool the carrier of T2 c= bool ( the carrier of T1 \/ the carrier of T2) by XBOOLE_1:7, ZFMISC_1:67;
A3: the topology of T1 c= bool ( the carrier of T1 \/ the carrier of T2) by A1, XBOOLE_1:1;
 the topology of T2 c= bool ( the carrier of T1 \/ the carrier of T2) by A2, XBOOLE_1:1;
then reconsider t = the topology of T1 \/ the topology of T2 as Subset-Family of ( the carrier of T1 \/ the carrier of T2) by A3, XBOOLE_1:8;
reconsider t = t as Subset-Family of ( the carrier of T1 \/ the carrier of T2) ;
set S = TopStruct(# ( the carrier of T1 \/ the carrier of T2),t #);
consider T being TopExtension of TopStruct(# ( the carrier of T1 \/ the carrier of T2),t #) such that
A4: T is strict and
A5: t is prebasis of T by Th53;
reconsider T = T as strict TopExtension of TopStruct(# ( the carrier of T1 \/ the carrier of T2),t #) by A4;
take  T ; ::_thesis: ( the carrier of T = the carrier of T1 \/ the carrier of T2 & the topology of T1 \/ the topology of T2 is prebasis of T )
thus  ( the carrier of T = the carrier of T1 \/ the carrier of T2 & the topology of T1 \/ the topology of T2 is prebasis of T ) by A5, Def5; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines Refinement YELLOW_9:def_6_:_
 for T1, T2 being TopStruct
for b3 being TopSpace holds
( b3 is Refinement of T1,T2 iff ( the carrier of b3 = the carrier of T1 \/ the carrier of T2 & the topology of T1 \/ the topology of T2 is prebasis of b3 ) );

registration
let T1 be non empty TopStruct ;
let T2 be TopStruct ;
cluster  ->  non empty for Refinement of T1,T2;
coherence
 for b1 being Refinement of T1,T2 holds not b1 is empty
proof
let T be Refinement of T1,T2; ::_thesis: not T is empty
 the carrier of T = the carrier of T2 \/ the carrier of T1 by Def6;
hence  not the carrier of T is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
cluster  ->  non empty for Refinement of T2,T1;
coherence
 for b1 being Refinement of T2,T1 holds not b1 is empty
proof
let T be Refinement of T2,T1; ::_thesis: not T is empty
 the carrier of T = the carrier of T2 \/ the carrier of T1 by Def6;
hence  not the carrier of T is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

theorem :: YELLOW_9:54
for T1, T2 being TopStruct
for T, T9 being Refinement of T1,T2 holds TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of T9, the topology of T9 #)
proof
let T1, T2 be TopStruct ; ::_thesis: for T, T9 being Refinement of T1,T2 holds TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of T9, the topology of T9 #)
let T, T9 be Refinement of T1,T2; ::_thesis: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of T9, the topology of T9 #)
A1: the carrier of T = the carrier of T1 \/ the carrier of T2 by Def6;
A2: the topology of T1 \/ the topology of T2 is prebasis of T by Def6;
A3: the carrier of T9 = the carrier of T1 \/ the carrier of T2 by Def6;
 the topology of T1 \/ the topology of T2 is prebasis of T9 by Def6;
hence  TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of T9, the topology of T9 #) by A1, A2, A3, Th26; ::_thesis: verum
end;

theorem :: YELLOW_9:55
for T1, T2 being TopStruct
for T being Refinement of T1,T2 holds T is Refinement of T2,T1
proof
let T1, T2 be TopStruct ; ::_thesis: for T being Refinement of T1,T2 holds T is Refinement of T2,T1
let T be Refinement of T1,T2; ::_thesis: T is Refinement of T2,T1
A1: the carrier of T = the carrier of T1 \/ the carrier of T2 by Def6;
 the topology of T1 \/ the topology of T2 is prebasis of T by Def6;
hence  T is Refinement of T2,T1 by A1, Def6; ::_thesis: verum
end;

theorem :: YELLOW_9:56
for T1, T2 being TopStruct
for T being Refinement of T1,T2
for X being Subset-Family of T st X = the topology of T1 \/ the topology of T2 holds
the topology of T = UniCl (FinMeetCl X)
proof
let T1, T2 be TopStruct ; ::_thesis: for T being Refinement of T1,T2
for X being Subset-Family of T st X = the topology of T1 \/ the topology of T2 holds
the topology of T = UniCl (FinMeetCl X)
let T be Refinement of T1,T2; ::_thesis: for X being Subset-Family of T st X = the topology of T1 \/ the topology of T2 holds
the topology of T = UniCl (FinMeetCl X)
let X be Subset-Family of T; ::_thesis: ( X = the topology of T1 \/ the topology of T2 implies the topology of T = UniCl (FinMeetCl X) )
assume  X = the topology of T1 \/ the topology of T2 ; ::_thesis: the topology of T = UniCl (FinMeetCl X)
then  X is prebasis of T by Def6;
then  FinMeetCl X is Basis of T by Th23;
hence  the topology of T = UniCl (FinMeetCl X) by Th22; ::_thesis: verum
end;

theorem :: YELLOW_9:57
for T1, T2 being TopStruct st the carrier of T1 = the carrier of T2 holds
for T being Refinement of T1,T2 holds
( T is TopExtension of T1 & T is TopExtension of T2 )
proof
let T1, T2 be TopStruct ; ::_thesis: ( the carrier of T1 = the carrier of T2 implies for T being Refinement of T1,T2 holds
( T is TopExtension of T1 & T is TopExtension of T2 ) )
assume A1: the carrier of T1 = the carrier of T2 ; ::_thesis: for T being Refinement of T1,T2 holds
( T is TopExtension of T1 & T is TopExtension of T2 )
let T be Refinement of T1,T2; ::_thesis: ( T is TopExtension of T1 & T is TopExtension of T2 )
A2: the carrier of T = the carrier of T1 \/ the carrier of T2 by Def6
.= the carrier of T1 by A1 ;
A3: the topology of T1 \/ the topology of T2 is prebasis of T by Def6;
A4: the topology of T1 c= the topology of T1 \/ the topology of T2 by XBOOLE_1:7;
A5: the topology of T2 c= the topology of T1 \/ the topology of T2 by XBOOLE_1:7;
A6: the topology of T1 \/ the topology of T2 c= the topology of T by A3, TOPS_2:64;
then A7: the topology of T1 c= the topology of T by A4, XBOOLE_1:1;
 the topology of T2 c= the topology of T by A5, A6, XBOOLE_1:1;
hence  ( T is TopExtension of T1 & T is TopExtension of T2 ) by A1, A2, A7, Def5; ::_thesis: verum
end;

theorem :: YELLOW_9:58
for T1, T2 being non empty TopSpace
for T being Refinement of T1,T2
for B1 being prebasis of T1
for B2 being prebasis of T2 holds (B1 \/ B2) \/ { the carrier of T1, the carrier of T2} is prebasis of T
proof
let T1, T2 be non empty TopSpace; ::_thesis: for T being Refinement of T1,T2
for B1 being prebasis of T1
for B2 being prebasis of T2 holds (B1 \/ B2) \/ { the carrier of T1, the carrier of T2} is prebasis of T
let T be Refinement of T1,T2; ::_thesis: for B1 being prebasis of T1
for B2 being prebasis of T2 holds (B1 \/ B2) \/ { the carrier of T1, the carrier of T2} is prebasis of T
let B1 be prebasis of T1; ::_thesis: for B2 being prebasis of T2 holds (B1 \/ B2) \/ { the carrier of T1, the carrier of T2} is prebasis of T
let B2 be prebasis of T2; ::_thesis: (B1 \/ B2) \/ { the carrier of T1, the carrier of T2} is prebasis of T
reconsider B = the topology of T1 \/ the topology of T2 as prebasis of T by Def6;
set cT1 = the carrier of T1;
set cT2 = the carrier of T2;
reconsider C1 = B1 \/ { the carrier of T1} as prebasis of T1 by Th29;
reconsider C2 = B2 \/ { the carrier of T2} as prebasis of T2 by Th29;
A1: B1 c= the topology of T1 by TOPS_2:64;
A2: C1 c= the topology of T1 by TOPS_2:64;
A3: B2 c= the topology of T2 by TOPS_2:64;
A4: C2 c= the topology of T2 by TOPS_2:64;
A5: the carrier of T1 in the topology of T1 by PRE_TOPC:def_1;
A6: the carrier of T2 in the topology of T2 by PRE_TOPC:def_1;
A7: B1 \/ B2 c= B by A1, A3, XBOOLE_1:13;
A8: B c= the topology of T by TOPS_2:64;
A9: the carrier of T1 in B by A5, XBOOLE_0:def_3;
A10: the carrier of T2 in B by A6, XBOOLE_0:def_3;
A11: B1 \/ B2 c= the topology of T by A7, A8, XBOOLE_1:1;
A12: { the carrier of T1, the carrier of T2} c= the topology of T by A8, A9, A10, ZFMISC_1:32;
A13: { the carrier of T1, the carrier of T2} c= B by A9, A10, ZFMISC_1:32;
 (B1 \/ B2) \/ { the carrier of T1, the carrier of T2} c= the topology of T by A11, A12, XBOOLE_1:8;
then reconsider BB = (B1 \/ B2) \/ { the carrier of T1, the carrier of T2} as Subset-Family of T by XBOOLE_1:1;
A14: the topology of T1 c= B by XBOOLE_1:7;
A15: the topology of T2 c= B by XBOOLE_1:7;
A16: C1 c= B by A2, A14, XBOOLE_1:1;
 C2 c= B by A4, A15, XBOOLE_1:1;
then reconsider D1 = C1, D2 = C2 as Subset-Family of T by A16, XBOOLE_1:1;
reconsider D1 = D1, D2 = D2 as Subset-Family of T ;
reconsider D1 = D1, D2 = D2 as Subset-Family of T ;
A17: UniCl (FinMeetCl BB) = UniCl (FinMeetCl (FinMeetCl BB)) by CANTOR_1:11
.= UniCl (FinMeetCl (UniCl (FinMeetCl BB))) by Th21 ;
A18: FinMeetCl B is Basis of T by Th23;
A19: FinMeetCl C1 is Basis of T1 by Th23;
A20: FinMeetCl C2 is Basis of T2 by Th23;
A21: UniCl (FinMeetCl B) = the topology of T by A18, Th22;
A22: UniCl (FinMeetCl C1) = the topology of T1 by A19, Th22;
A23: UniCl (FinMeetCl C2) = the topology of T2 by A20, Th22;
A24: B1 c= B1 \/ B2 by XBOOLE_1:7;
A25: B2 c= B1 \/ B2 by XBOOLE_1:7;
A26: { the carrier of T1} c= { the carrier of T1, the carrier of T2} by ZFMISC_1:7;
A27: { the carrier of T2} c= { the carrier of T1, the carrier of T2} by ZFMISC_1:7;
A28: D1 c= BB by A24, A26, XBOOLE_1:13;
A29: D2 c= BB by A25, A27, XBOOLE_1:13;
 BB c= B by A7, A13, XBOOLE_1:8;
then A30: FinMeetCl BB c= FinMeetCl B by CANTOR_1:14;
A31: FinMeetCl D1 c= FinMeetCl BB by A28, CANTOR_1:14;
A32: FinMeetCl D2 c= FinMeetCl BB by A29, CANTOR_1:14;
A33: UniCl (FinMeetCl BB) c= the topology of T by A21, A30, CANTOR_1:9;
A34: the carrier of T1 in { the carrier of T1} by TARSKI:def_1;
A35: the carrier of T2 in { the carrier of T2} by TARSKI:def_1;
A36: the carrier of T1 in C1 by A34, XBOOLE_0:def_3;
A37: the carrier of T2 in C2 by A35, XBOOLE_0:def_3;
A38: FinMeetCl D1 = { the carrier of T} \/ (FinMeetCl C1) by A36, Th20;
A39: FinMeetCl D2 = { the carrier of T} \/ (FinMeetCl C2) by A37, Th20;
A40: FinMeetCl C1 c= FinMeetCl D1 by A38, XBOOLE_1:7;
A41: FinMeetCl C2 c= FinMeetCl D2 by A39, XBOOLE_1:7;
A42: FinMeetCl C1 c= FinMeetCl BB by A31, A40, XBOOLE_1:1;
A43: FinMeetCl C2 c= FinMeetCl BB by A32, A41, XBOOLE_1:1;
A44: the topology of T1 c= UniCl (FinMeetCl BB) by A22, A42, Th19;
 the topology of T2 c= UniCl (FinMeetCl BB) by A23, A43, Th19;
then  B c= UniCl (FinMeetCl BB) by A44, XBOOLE_1:8;
then  FinMeetCl B c= FinMeetCl (UniCl (FinMeetCl BB)) by CANTOR_1:14;
then  the topology of T c= UniCl (FinMeetCl BB) by A17, A21, CANTOR_1:9;
then  the topology of T = UniCl (FinMeetCl BB) by A33, XBOOLE_0:def_10;
then  FinMeetCl BB is Basis of T by Th22;
hence  (B1 \/ B2) \/ { the carrier of T1, the carrier of T2} is prebasis of T by Th23; ::_thesis: verum
end;

theorem Th59: :: YELLOW_9:59
for T1, T2 being non empty TopSpace
for B1 being Basis of T1
for B2 being Basis of T2
for T being Refinement of T1,T2 holds (B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T
proof
let T1, T2 be non empty TopSpace; ::_thesis: for B1 being Basis of T1
for B2 being Basis of T2
for T being Refinement of T1,T2 holds (B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T
let B1 be Basis of T1; ::_thesis: for B2 being Basis of T2
for T being Refinement of T1,T2 holds (B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T
let B2 be Basis of T2; ::_thesis: for T being Refinement of T1,T2 holds (B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T
let T be Refinement of T1,T2; ::_thesis: (B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T
set BB = (B1 \/ B2) \/ (INTERSECTION (B1,B2));
reconsider B = the topology of T1 \/ the topology of T2 as prebasis of T by Def6;
A1: FinMeetCl B is Basis of T by Th23;
A2: the carrier of T1 \/ the carrier of T2 = the carrier of T by Def6;
A3: B1 c= the topology of T1 by TOPS_2:64;
A4: B2 c= the topology of T2 by TOPS_2:64;
A5: the topology of T1 c= B by XBOOLE_1:7;
A6: the topology of T2 c= B by XBOOLE_1:7;
A7: B1 c= B by A3, A5, XBOOLE_1:1;
A8: B2 c= B by A4, A6, XBOOLE_1:1;
A9: B c= FinMeetCl B by CANTOR_1:4;
then A10: B1 c= FinMeetCl B by A7, XBOOLE_1:1;
A11: B2 c= FinMeetCl B by A8, A9, XBOOLE_1:1;
A12: B1 \/ B2 c= B by A3, A4, XBOOLE_1:13;
A13: INTERSECTION (B1,B2) c= FinMeetCl B by A10, A11, CANTOR_1:13;
 B1 \/ B2 c= FinMeetCl B by A9, A12, XBOOLE_1:1;
then A14: (B1 \/ B2) \/ (INTERSECTION (B1,B2)) c= FinMeetCl B by A13, XBOOLE_1:8;
A15: FinMeetCl B c= the topology of T by A1, TOPS_2:64;
reconsider BB = (B1 \/ B2) \/ (INTERSECTION (B1,B2)) as Subset-Family of T by A14, XBOOLE_1:1;
now__::_thesis:_for_A_being_Subset_of_T_st_A_is_open_holds_
for_p_being_Point_of_T_st_p_in_A_holds_
ex_a_being_Subset_of_T_st_
(_a_in_BB_&_p_in_a_&_a_c=_A_)
let A be Subset of T; ::_thesis: ( A is open implies for p being Point of T st p in A holds
ex a being Subset of T st
( a in BB & p in a & a c= A ) )
assume A16: A is open ; ::_thesis: for p being Point of T st p in A holds
ex a being Subset of T st
( a in BB & p in a & a c= A )
let p be Point of T; ::_thesis: ( p in A implies ex a being Subset of T st
( a in BB & p in a & a c= A ) )
assume  p in A ; ::_thesis: ex a being Subset of T st
( a in BB & p in a & a c= A )
then consider a being Subset of T such that
A17: a in FinMeetCl B and
A18: p in a and
A19: a c= A by A1, A16, Th31;
consider Y being Subset-Family of T such that
A20: Y c= B and
A21: Y is finite and
A22: a = Intersect Y by A17, CANTOR_1:def_3;
reconsider Y1 = Y /\ the topology of T1 as Subset-Family of T1 ;
reconsider Y2 = Y /\ the topology of T2 as Subset-Family of T2 ;
A23: Y = B /\ Y by A20, XBOOLE_1:28
.= Y1 \/ Y2 by XBOOLE_1:23 ;
 the carrier of T1 c= the carrier of T1 ;
then reconsider cT1 = the carrier of T1 as Subset of T1 ;
 the carrier of T2 c= the carrier of T2 ;
then reconsider cT2 = the carrier of T2 as Subset of T2 ;
A24: cT1 in the topology of T1 by PRE_TOPC:def_1;
A25: cT2 in the topology of T2 by PRE_TOPC:def_1;
A26: cT1 is open by A24, PRE_TOPC:def_2;
A27: cT2 is open by A25, PRE_TOPC:def_2;
thus  ex a being Subset of T st
( a in BB & p in a & a c= A ) ::_thesis: verum
proof
percases ( ( Y1 \/ Y2 = {} & p in cT1 ) or ( Y1 \/ Y2 = {} & p in cT2 ) or ( Y1 = {} & Y2 <> {} & Y <> {} ) or ( Y1 <> {} & Y2 = {} & Y <> {} ) or ( Y1 <> {} & Y2 <> {} & Y <> {} ) ) by A2, XBOOLE_0:def_3;
supposeA28: ( Y1 \/ Y2 = {} & p in cT1 ) ; ::_thesis: ex a being Subset of T st
( a in BB & p in a & a c= A )
then consider b1 being Subset of T1 such that
A29: b1 in B1 and
A30: p in b1 and
 b1 c= cT1 by A26, Th31;
A31: b1 in B1 \/ B2 by A29, XBOOLE_0:def_3;
A32: a = the carrier of T by A22, A23, A28, SETFAM_1:def_9;
 b1 in BB by A31, XBOOLE_0:def_3;
hence  ex a being Subset of T st
( a in BB & p in a & a c= A ) by A19, A30, A32, XBOOLE_1:1; ::_thesis: verum
end;
supposeA33: ( Y1 \/ Y2 = {} & p in cT2 ) ; ::_thesis: ex a being Subset of T st
( a in BB & p in a & a c= A )
then consider b2 being Subset of T2 such that
A34: b2 in B2 and
A35: p in b2 and
 b2 c= cT2 by A27, Th31;
A36: b2 in B1 \/ B2 by A34, XBOOLE_0:def_3;
A37: a = the carrier of T by A22, A23, A33, SETFAM_1:def_9;
 b2 in BB by A36, XBOOLE_0:def_3;
hence  ex a being Subset of T st
( a in BB & p in a & a c= A ) by A19, A35, A37, XBOOLE_1:1; ::_thesis: verum
end;
supposeA38: ( Y1 = {} & Y2 <> {} & Y <> {} ) ; ::_thesis: ex a being Subset of T st
( a in BB & p in a & a c= A )
then A39: a = meet Y2 by A22, A23, SETFAM_1:def_9
.= Intersect Y2 by A38, SETFAM_1:def_9 ;
 Y2 c= the topology of T2 by XBOOLE_1:17;
then  a in FinMeetCl the topology of T2 by A21, A39, CANTOR_1:def_3;
then A40: a in the topology of T2 by CANTOR_1:5;
 the topology of T2 = UniCl B2 by Th22;
then consider Z being Subset-Family of T2 such that
A41: Z c= B2 and
A42: a = union Z by A40, CANTOR_1:def_1;
consider z being set  such that
A43: p in z and
A44: z in Z by A18, A42, TARSKI:def_4;
 z in B1 \/ B2 by A41, A44, XBOOLE_0:def_3;
then A45: z in BB by XBOOLE_0:def_3;
 z c= a by A42, A44, ZFMISC_1:74;
hence  ex a being Subset of T st
( a in BB & p in a & a c= A ) by A19, A43, A45, XBOOLE_1:1; ::_thesis: verum
end;
supposeA46: ( Y1 <> {} & Y2 = {} & Y <> {} ) ; ::_thesis: ex a being Subset of T st
( a in BB & p in a & a c= A )
then A47: a = meet Y1 by A22, A23, SETFAM_1:def_9
.= Intersect Y1 by A46, SETFAM_1:def_9 ;
 Y1 c= the topology of T1 by XBOOLE_1:17;
then  a in FinMeetCl the topology of T1 by A21, A47, CANTOR_1:def_3;
then A48: a in the topology of T1 by CANTOR_1:5;
 the topology of T1 = UniCl B1 by Th22;
then consider Z being Subset-Family of T1 such that
A49: Z c= B1 and
A50: a = union Z by A48, CANTOR_1:def_1;
consider z being set  such that
A51: p in z and
A52: z in Z by A18, A50, TARSKI:def_4;
 z in B1 \/ B2 by A49, A52, XBOOLE_0:def_3;
then A53: z in BB by XBOOLE_0:def_3;
 z c= a by A50, A52, ZFMISC_1:74;
hence  ex a being Subset of T st
( a in BB & p in a & a c= A ) by A19, A51, A53, XBOOLE_1:1; ::_thesis: verum
end;
supposeA54: ( Y1 <> {} & Y2 <> {} & Y <> {} ) ; ::_thesis: ex a being Subset of T st
( a in BB & p in a & a c= A )
then A55: a = meet Y by A22, SETFAM_1:def_9
.= (meet Y1) /\ (meet Y2) by A23, A54, SETFAM_1:9
.= (meet Y1) /\ (Intersect Y2) by A54, SETFAM_1:def_9
.= (Intersect Y1) /\ (Intersect Y2) by A54, SETFAM_1:def_9 ;
A56: Y1 c= the topology of T1 by XBOOLE_1:17;
A57: Y2 c= the topology of T2 by XBOOLE_1:17;
A58: Intersect Y1 in FinMeetCl the topology of T1 by A21, A56, CANTOR_1:def_3;
A59: Intersect Y2 in FinMeetCl the topology of T2 by A21, A57, CANTOR_1:def_3;
A60: Intersect Y1 in the topology of T1 by A58, CANTOR_1:5;
A61: the topology of T1 = UniCl B1 by Th22;
A62: Intersect Y2 in the topology of T2 by A59, CANTOR_1:5;
A63: the topology of T2 = UniCl B2 by Th22;
consider Z1 being Subset-Family of T1 such that
A64: Z1 c= B1 and
A65: Intersect Y1 = union Z1 by A60, A61, CANTOR_1:def_1;
 p in Intersect Y1 by A18, A55, XBOOLE_0:def_4;
then consider z1 being set  such that
A66: p in z1 and
A67: z1 in Z1 by A65, TARSKI:def_4;
consider Z2 being Subset-Family of T2 such that
A68: Z2 c= B2 and
A69: Intersect Y2 = union Z2 by A62, A63, CANTOR_1:def_1;
 p in Intersect Y2 by A18, A55, XBOOLE_0:def_4;
then consider z2 being set  such that
A70: p in z2 and
A71: z2 in Z2 by A69, TARSKI:def_4;
A72: z1 /\ z2 in INTERSECTION (B1,B2) by A64, A67, A68, A71, SETFAM_1:def_5;
A73: z1 c= union Z1 by A67, ZFMISC_1:74;
A74: z2 c= union Z2 by A71, ZFMISC_1:74;
A75: z1 /\ z2 in BB by A72, XBOOLE_0:def_3;
A76: z1 /\ z2 c= a by A55, A65, A69, A73, A74, XBOOLE_1:27;
 p in z1 /\ z2 by A66, A70, XBOOLE_0:def_4;
hence  ex a being Subset of T st
( a in BB & p in a & a c= A ) by A19, A75, A76, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
end;
hence  (B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T by A14, A15, Th32, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th60: :: YELLOW_9:60
for T1, T2 being non empty TopSpace st the carrier of T1 = the carrier of T2 holds
for T being Refinement of T1,T2 holds INTERSECTION ( the topology of T1, the topology of T2) is Basis of T
proof
let T1, T2 be non empty TopSpace; ::_thesis: ( the carrier of T1 = the carrier of T2 implies for T being Refinement of T1,T2 holds INTERSECTION ( the topology of T1, the topology of T2) is Basis of T )
assume A1: the carrier of T1 = the carrier of T2 ; ::_thesis: for T being Refinement of T1,T2 holds INTERSECTION ( the topology of T1, the topology of T2) is Basis of T
let T be Refinement of T1,T2; ::_thesis: INTERSECTION ( the topology of T1, the topology of T2) is Basis of T
set B1 = the topology of T1;
set B2 = the topology of T2;
 UniCl the topology of T1 = the topology of T1 by CANTOR_1:6;
then reconsider B1 = the topology of T1 as Basis of T1 by Th22;
 UniCl the topology of T2 = the topology of T2 by CANTOR_1:6;
then reconsider B2 = the topology of T2 as Basis of T2 by Th22;
A2: (B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T by Th59;
A3: the carrier of T1 in B1 by PRE_TOPC:def_1;
A4: the carrier of T2 in B2 by PRE_TOPC:def_1;
A5: B1 c= INTERSECTION (B1,B2)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B1 or a in INTERSECTION (B1,B2) )
assume A6: a in B1 ; ::_thesis: a in INTERSECTION (B1,B2)
then  a /\ the carrier of T1 in INTERSECTION (B1,B2) by A1, A4, SETFAM_1:def_5;
hence  a in INTERSECTION (B1,B2) by A6, XBOOLE_1:28; ::_thesis: verum
end;
 B2 c= INTERSECTION (B1,B2)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B2 or a in INTERSECTION (B1,B2) )
assume A7: a in B2 ; ::_thesis: a in INTERSECTION (B1,B2)
then  a /\ the carrier of T2 in INTERSECTION (B1,B2) by A1, A3, SETFAM_1:def_5;
hence  a in INTERSECTION (B1,B2) by A7, XBOOLE_1:28; ::_thesis: verum
end;
hence  INTERSECTION ( the topology of T1, the topology of T2) is Basis of T by A2, A5, XBOOLE_1:8, XBOOLE_1:12; ::_thesis: verum
end;

theorem :: YELLOW_9:61
for L being non empty RelStr
for T1, T2 being correct TopAugmentation of L
for T being Refinement of T1,T2 holds INTERSECTION ( the topology of T1, the topology of T2) is Basis of T
proof
let L be non empty RelStr ; ::_thesis: for T1, T2 being correct TopAugmentation of L
for T being Refinement of T1,T2 holds INTERSECTION ( the topology of T1, the topology of T2) is Basis of T
let T1, T2 be correct TopAugmentation of L; ::_thesis: for T being Refinement of T1,T2 holds INTERSECTION ( the topology of T1, the topology of T2) is Basis of T
A1: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of L, the InternalRel of L #) by Def4;
 RelStr(# the carrier of T2, the InternalRel of T2 #) = RelStr(# the carrier of L, the InternalRel of L #) by Def4;
hence  for T being Refinement of T1,T2 holds INTERSECTION ( the topology of T1, the topology of T2) is Basis of T by A1, Th60; ::_thesis: verum
end;