:: 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;