:: TDLAT_2 semantic presentation begin theorem Th1: :: TDLAT_2:1 for T being TopSpace for A being Subset of T holds ( Int (Cl (Int A)) c= Int (Cl A) & Int (Cl (Int A)) c= Cl (Int A) ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( Int (Cl (Int A)) c= Int (Cl A) & Int (Cl (Int A)) c= Cl (Int A) ) let A be Subset of T; ::_thesis: ( Int (Cl (Int A)) c= Int (Cl A) & Int (Cl (Int A)) c= Cl (Int A) ) Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16; hence Int (Cl (Int A)) c= Int (Cl A) by TOPS_1:19; ::_thesis: Int (Cl (Int A)) c= Cl (Int A) thus Int (Cl (Int A)) c= Cl (Int A) by TOPS_1:16; ::_thesis: verum end; theorem Th2: :: TDLAT_2:2 for T being TopSpace for A being Subset of T holds ( Cl (Int A) c= Cl (Int (Cl A)) & Int (Cl A) c= Cl (Int (Cl A)) ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( Cl (Int A) c= Cl (Int (Cl A)) & Int (Cl A) c= Cl (Int (Cl A)) ) let A be Subset of T; ::_thesis: ( Cl (Int A) c= Cl (Int (Cl A)) & Int (Cl A) c= Cl (Int (Cl A)) ) Int A c= Int (Cl A) by PRE_TOPC:18, TOPS_1:19; hence Cl (Int A) c= Cl (Int (Cl A)) by PRE_TOPC:19; ::_thesis: Int (Cl A) c= Cl (Int (Cl A)) thus Int (Cl A) c= Cl (Int (Cl A)) by PRE_TOPC:18; ::_thesis: verum end; theorem :: TDLAT_2:3 for T being TopSpace for A, B being Subset of T st B is closed & Cl (Int (A /\ B)) = A holds A c= B proof let T be TopSpace; ::_thesis: for A, B being Subset of T st B is closed & Cl (Int (A /\ B)) = A holds A c= B let A, B be Subset of T; ::_thesis: ( B is closed & Cl (Int (A /\ B)) = A implies A c= B ) assume A1: B is closed ; ::_thesis: ( not Cl (Int (A /\ B)) = A or A c= B ) A2: A /\ B c= B by XBOOLE_1:17; Int (A /\ B) c= A /\ B by TOPS_1:16; then Int (A /\ B) c= B by A2, XBOOLE_1:1; then A3: Cl (Int (A /\ B)) c= Cl B by PRE_TOPC:19; assume Cl (Int (A /\ B)) = A ; ::_thesis: A c= B hence A c= B by A1, A3, PRE_TOPC:22; ::_thesis: verum end; theorem Th4: :: TDLAT_2:4 for T being TopSpace for A, B being Subset of T st A is open & Int (Cl (A \/ B)) = B holds A c= B proof let T be TopSpace; ::_thesis: for A, B being Subset of T st A is open & Int (Cl (A \/ B)) = B holds A c= B let A, B be Subset of T; ::_thesis: ( A is open & Int (Cl (A \/ B)) = B implies A c= B ) assume A1: A is open ; ::_thesis: ( not Int (Cl (A \/ B)) = B or A c= B ) A2: A c= A \/ B by XBOOLE_1:7; A \/ B c= Cl (A \/ B) by PRE_TOPC:18; then A c= Cl (A \/ B) by A2, XBOOLE_1:1; then A3: Int A c= Int (Cl (A \/ B)) by TOPS_1:19; assume Int (Cl (A \/ B)) = B ; ::_thesis: A c= B hence A c= B by A1, A3, TOPS_1:23; ::_thesis: verum end; theorem Th5: :: TDLAT_2:5 for T being TopSpace for A being Subset of T st A c= Cl (Int A) holds A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A)))) proof let T be TopSpace; ::_thesis: for A being Subset of T st A c= Cl (Int A) holds A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A)))) let A be Subset of T; ::_thesis: ( A c= Cl (Int A) implies A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A)))) ) assume A1: A c= Cl (Int A) ; ::_thesis: A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A)))) A2: Int (Cl A) c= Cl (Int (Cl A)) by PRE_TOPC:18; A3: Int A c= Int (Cl A) by PRE_TOPC:18, TOPS_1:19; then Cl (Int A) c= Cl (Int (Cl A)) by PRE_TOPC:19; then A c= Cl (Int (Cl A)) by A1, XBOOLE_1:1; then A \/ (Int (Cl A)) c= (Cl (Int (Cl A))) \/ (Cl (Int (Cl A))) by A2, XBOOLE_1:13; then A4: A \/ (Int (Cl A)) c= Cl ((Int A) \/ (Int (Cl A))) by A3, XBOOLE_1:12; (Int A) \/ (Int (Int (Cl A))) c= Int (A \/ (Int (Cl A))) by TOPS_1:20; then Cl ((Int A) \/ (Int (Cl A))) c= Cl (Int (A \/ (Int (Cl A)))) by PRE_TOPC:19; hence A \/ (Int (Cl A)) c= Cl (Int (A \/ (Int (Cl A)))) by A4, XBOOLE_1:1; ::_thesis: verum end; theorem Th6: :: TDLAT_2:6 for T being TopSpace for A being Subset of T st Int (Cl A) c= A holds Int (Cl (A /\ (Cl (Int A)))) c= A /\ (Cl (Int A)) proof let T be TopSpace; ::_thesis: for A being Subset of T st Int (Cl A) c= A holds Int (Cl (A /\ (Cl (Int A)))) c= A /\ (Cl (Int A)) let A be Subset of T; ::_thesis: ( Int (Cl A) c= A implies Int (Cl (A /\ (Cl (Int A)))) c= A /\ (Cl (Int A)) ) assume A1: Int (Cl A) c= A ; ::_thesis: Int (Cl (A /\ (Cl (Int A)))) c= A /\ (Cl (Int A)) A2: Int (Cl (Int A)) c= Cl (Int A) by TOPS_1:16; A3: Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16; then Int (Cl (Int A)) c= Int (Cl A) by TOPS_1:19; then Int (Cl (Int A)) c= A by A1, XBOOLE_1:1; then (Int (Cl (Int A))) /\ (Int (Cl (Int A))) c= A /\ (Cl (Int A)) by A2, XBOOLE_1:27; then A4: Int ((Cl A) /\ (Cl (Int A))) c= A /\ (Cl (Int A)) by A3, XBOOLE_1:28; Cl (A /\ (Cl (Int A))) c= (Cl A) /\ (Cl (Cl (Int A))) by PRE_TOPC:21; then Int (Cl (A /\ (Cl (Int A)))) c= Int ((Cl A) /\ (Cl (Int A))) by TOPS_1:19; hence Int (Cl (A /\ (Cl (Int A)))) c= A /\ (Cl (Int A)) by A4, XBOOLE_1:1; ::_thesis: verum end; begin notation let T be TopSpace; let F be Subset-Family of T; synonym Cl F for clf F; end; theorem Th7: :: TDLAT_2:7 for T being TopSpace for F being Subset-Family of T holds Cl F = { A where A is Subset of T : ex B being Subset of T st ( A = Cl B & B in F ) } proof let T be TopSpace; ::_thesis: for F being Subset-Family of T holds Cl F = { A where A is Subset of T : ex B being Subset of T st ( A = Cl B & B in F ) } let F be Subset-Family of T; ::_thesis: Cl F = { A where A is Subset of T : ex B being Subset of T st ( A = Cl B & B in F ) } set P = { A where A is Subset of T : ex B being Subset of T st ( A = Cl B & B in F ) } ; now__::_thesis:_for_C_being_set_st_C_in__{__A_where_A_is_Subset_of_T_:_ex_B_being_Subset_of_T_st_ (_A_=_Cl_B_&_B_in_F_)__}__holds_ C_in_bool_the_carrier_of_T let C be set ; ::_thesis: ( C in { A where A is Subset of T : ex B being Subset of T st ( A = Cl B & B in F ) } implies C in bool the carrier of T ) assume C in { A where A is Subset of T : ex B being Subset of T st ( A = Cl B & B in F ) } ; ::_thesis: C in bool the carrier of T then ex A being Subset of T st ( C = A & ex B being Subset of T st ( A = Cl B & B in F ) ) ; hence C in bool the carrier of T ; ::_thesis: verum end; then reconsider P = { A where A is Subset of T : ex B being Subset of T st ( A = Cl B & B in F ) } as Subset-Family of T by TARSKI:def_3; reconsider P = P as Subset-Family of T ; for X being set holds ( X in Cl F iff X in P ) proof let X be set ; ::_thesis: ( X in Cl F iff X in P ) A1: now__::_thesis:_(_X_in_P_implies_X_in_Cl_F_) assume A2: X in P ; ::_thesis: X in Cl F then reconsider C = X as Subset of T ; ex D being Subset of T st ( D = C & ex B being Subset of T st ( D = Cl B & B in F ) ) by A2; hence X in Cl F by PCOMPS_1:def_2; ::_thesis: verum end; now__::_thesis:_(_X_in_Cl_F_implies_X_in_P_) assume A3: X in Cl F ; ::_thesis: X in P then reconsider C = X as Subset of T ; ex B being Subset of T st ( C = Cl B & B in F ) by A3, PCOMPS_1:def_2; hence X in P ; ::_thesis: verum end; hence ( X in Cl F iff X in P ) by A1; ::_thesis: verum end; hence Cl F = { A where A is Subset of T : ex B being Subset of T st ( A = Cl B & B in F ) } by TARSKI:1; ::_thesis: verum end; theorem :: TDLAT_2:8 for T being TopSpace for F being Subset-Family of T holds Cl F = Cl (Cl F) proof let T be TopSpace; ::_thesis: for F being Subset-Family of T holds Cl F = Cl (Cl F) let F be Subset-Family of T; ::_thesis: Cl F = Cl (Cl F) A1: Cl (Cl F) = { D where D is Subset of T : ex B being Subset of T st ( D = Cl B & B in Cl F ) } by Th7; A2: Cl F = { A where A is Subset of T : ex B being Subset of T st ( A = Cl B & B in F ) } by Th7; for X being set holds ( X in Cl F iff X in Cl (Cl F) ) proof let X be set ; ::_thesis: ( X in Cl F iff X in Cl (Cl F) ) A3: now__::_thesis:_(_X_in_Cl_F_implies_X_in_Cl_(Cl_F)_) assume A4: X in Cl F ; ::_thesis: X in Cl (Cl F) then reconsider C = X as Subset of T ; consider B being Subset of T such that A5: C = Cl B and A6: B in F by A4, PCOMPS_1:def_2; A7: Cl B in Cl F by A6, PCOMPS_1:def_2; C = Cl (Cl B) by A5; hence X in Cl (Cl F) by A1, A7; ::_thesis: verum end; now__::_thesis:_(_X_in_Cl_(Cl_F)_implies_X_in_Cl_F_) assume A8: X in Cl (Cl F) ; ::_thesis: X in Cl F then reconsider C = X as Subset of T ; ex Q being Subset of T st ( Q = C & ex B being Subset of T st ( Q = Cl B & B in Cl F ) ) by A1, A8; then consider B being Subset of T such that A9: C = Cl B and A10: B in Cl F ; ex Q being Subset of T st ( Q = B & ex R being Subset of T st ( Q = Cl R & R in F ) ) by A2, A10; hence X in Cl F by A9, PCOMPS_1:def_2; ::_thesis: verum end; hence ( X in Cl F iff X in Cl (Cl F) ) by A3; ::_thesis: verum end; hence Cl F = Cl (Cl F) by TARSKI:1; ::_thesis: verum end; theorem Th9: :: TDLAT_2:9 for T being TopSpace for F being Subset-Family of T holds ( F = {} iff Cl F = {} ) proof let T be TopSpace; ::_thesis: for F being Subset-Family of T holds ( F = {} iff Cl F = {} ) let F be Subset-Family of T; ::_thesis: ( F = {} iff Cl F = {} ) thus ( F = {} implies Cl F = {} ) by PCOMPS_1:12; ::_thesis: ( Cl F = {} implies F = {} ) assume A1: Cl F = {} ; ::_thesis: F = {} set B = the Element of F; assume A2: F <> {} ; ::_thesis: contradiction then reconsider B = the Element of F as Subset of T by TARSKI:def_3; Cl B in Cl F by A2, PCOMPS_1:def_2; hence contradiction by A1; ::_thesis: verum end; theorem :: TDLAT_2:10 for T being TopSpace for F, G being Subset-Family of T holds Cl (F /\ G) c= (Cl F) /\ (Cl G) proof let T be TopSpace; ::_thesis: for F, G being Subset-Family of T holds Cl (F /\ G) c= (Cl F) /\ (Cl G) let F, G be Subset-Family of T; ::_thesis: Cl (F /\ G) c= (Cl F) /\ (Cl G) for X being set st X in Cl (F /\ G) holds X in (Cl F) /\ (Cl G) proof let X be set ; ::_thesis: ( X in Cl (F /\ G) implies X in (Cl F) /\ (Cl G) ) assume A1: X in Cl (F /\ G) ; ::_thesis: X in (Cl F) /\ (Cl G) then reconsider X0 = X as Subset of T ; consider W being Subset of T such that A2: X0 = Cl W and A3: W in F /\ G by A1, PCOMPS_1:def_2; W in G by A3, XBOOLE_0:def_4; then A4: X0 in Cl G by A2, PCOMPS_1:def_2; W in F by A3, XBOOLE_0:def_4; then X0 in Cl F by A2, PCOMPS_1:def_2; hence X in (Cl F) /\ (Cl G) by A4, XBOOLE_0:def_4; ::_thesis: verum end; hence Cl (F /\ G) c= (Cl F) /\ (Cl G) by TARSKI:def_3; ::_thesis: verum end; theorem :: TDLAT_2:11 for T being TopSpace for F, G being Subset-Family of T holds (Cl F) \ (Cl G) c= Cl (F \ G) proof let T be TopSpace; ::_thesis: for F, G being Subset-Family of T holds (Cl F) \ (Cl G) c= Cl (F \ G) let F, G be Subset-Family of T; ::_thesis: (Cl F) \ (Cl G) c= Cl (F \ G) for X being set st X in (Cl F) \ (Cl G) holds X in Cl (F \ G) proof let X be set ; ::_thesis: ( X in (Cl F) \ (Cl G) implies X in Cl (F \ G) ) assume A1: X in (Cl F) \ (Cl G) ; ::_thesis: X in Cl (F \ G) then reconsider X0 = X as Subset of T ; X in Cl F by A1, XBOOLE_0:def_5; then consider W being Subset of T such that A2: X0 = Cl W and A3: W in F by PCOMPS_1:def_2; not X in Cl G by A1, XBOOLE_0:def_5; then not W in G by A2, PCOMPS_1:def_2; then W in F \ G by A3, XBOOLE_0:def_5; hence X in Cl (F \ G) by A2, PCOMPS_1:def_2; ::_thesis: verum end; hence (Cl F) \ (Cl G) c= Cl (F \ G) by TARSKI:def_3; ::_thesis: verum end; theorem :: TDLAT_2:12 for T being TopSpace for F being Subset-Family of T for A being Subset of T st A in F holds ( meet (Cl F) c= Cl A & Cl A c= union (Cl F) ) proof let T be TopSpace; ::_thesis: for F being Subset-Family of T for A being Subset of T st A in F holds ( meet (Cl F) c= Cl A & Cl A c= union (Cl F) ) let F be Subset-Family of T; ::_thesis: for A being Subset of T st A in F holds ( meet (Cl F) c= Cl A & Cl A c= union (Cl F) ) let A be Subset of T; ::_thesis: ( A in F implies ( meet (Cl F) c= Cl A & Cl A c= union (Cl F) ) ) assume A in F ; ::_thesis: ( meet (Cl F) c= Cl A & Cl A c= union (Cl F) ) then Cl A in { P where P is Subset of T : ex B being Subset of T st ( P = Cl B & B in F ) } ; then A1: Cl A in Cl F by Th7; hence meet (Cl F) c= Cl A by SETFAM_1:3; ::_thesis: Cl A c= union (Cl F) thus Cl A c= union (Cl F) by A1, ZFMISC_1:74; ::_thesis: verum end; theorem Th13: :: TDLAT_2:13 for T being TopSpace for F being Subset-Family of T holds meet F c= meet (Cl F) proof let T be TopSpace; ::_thesis: for F being Subset-Family of T holds meet F c= meet (Cl F) let F be Subset-Family of T; ::_thesis: meet F c= meet (Cl F) A1: for A being set st A in Cl F holds meet F c= A proof let A be set ; ::_thesis: ( A in Cl F implies meet F c= A ) assume A2: A in Cl F ; ::_thesis: meet F c= A then reconsider A0 = A as Subset of T ; consider B being Subset of T such that A3: A0 = Cl B and A4: B in F by A2, PCOMPS_1:def_2; A5: B c= A0 by A3, PRE_TOPC:18; meet F c= B by A4, SETFAM_1:3; hence meet F c= A by A5, XBOOLE_1:1; ::_thesis: verum end; now__::_thesis:_meet_F_c=_meet_(Cl_F) percases ( Cl F = {} or Cl F <> {} ) ; suppose Cl F = {} ; ::_thesis: meet F c= meet (Cl F) hence meet F c= meet (Cl F) by Th9; ::_thesis: verum end; suppose Cl F <> {} ; ::_thesis: meet F c= meet (Cl F) hence meet F c= meet (Cl F) by A1, SETFAM_1:5; ::_thesis: verum end; end; end; hence meet F c= meet (Cl F) ; ::_thesis: verum end; theorem Th14: :: TDLAT_2:14 for T being TopSpace for F being Subset-Family of T holds Cl (meet F) c= meet (Cl F) proof let T be TopSpace; ::_thesis: for F being Subset-Family of T holds Cl (meet F) c= meet (Cl F) let F be Subset-Family of T; ::_thesis: Cl (meet F) c= meet (Cl F) A1: meet (Cl F) is closed by PCOMPS_1:11, TOPS_2:22; Cl (meet F) c= Cl (meet (Cl F)) by Th13, PRE_TOPC:19; hence Cl (meet F) c= meet (Cl F) by A1, PRE_TOPC:22; ::_thesis: verum end; theorem Th15: :: TDLAT_2:15 for T being TopSpace for F being Subset-Family of T holds union (Cl F) c= Cl (union F) proof let T be TopSpace; ::_thesis: for F being Subset-Family of T holds union (Cl F) c= Cl (union F) let F be Subset-Family of T; ::_thesis: union (Cl F) c= Cl (union F) for A being set st A in Cl F holds A c= Cl (union F) proof let A be set ; ::_thesis: ( A in Cl F implies A c= Cl (union F) ) assume A1: A in Cl F ; ::_thesis: A c= Cl (union F) then reconsider A0 = A as Subset of T ; ex B being Subset of T st ( A0 = Cl B & B in F ) by A1, PCOMPS_1:def_2; hence A c= Cl (union F) by PRE_TOPC:19, ZFMISC_1:74; ::_thesis: verum end; hence union (Cl F) c= Cl (union F) by ZFMISC_1:76; ::_thesis: verum end; definition let T be TopSpace; let F be Subset-Family of T; func Int F -> Subset-Family of T means :Def1: :: TDLAT_2:def 1 for A being Subset of T holds ( A in it iff ex B being Subset of T st ( A = Int B & B in F ) ); existence ex b1 being Subset-Family of T st for A being Subset of T holds ( A in b1 iff ex B being Subset of T st ( A = Int B & B in F ) ) proof defpred S1[ Subset of T] means ex B being Subset of T st ( \$1 = Int B & B in F ); thus ex F being Subset-Family of T st for A being Subset of T holds ( A in F iff S1[A] ) from SUBSET_1:sch_3(); ::_thesis: verum end; uniqueness for b1, b2 being Subset-Family of T st ( for A being Subset of T holds ( A in b1 iff ex B being Subset of T st ( A = Int B & B in F ) ) ) & ( for A being Subset of T holds ( A in b2 iff ex B being Subset of T st ( A = Int B & B in F ) ) ) holds b1 = b2 proof let H, G be Subset-Family of T; ::_thesis: ( ( for A being Subset of T holds ( A in H iff ex B being Subset of T st ( A = Int B & B in F ) ) ) & ( for A being Subset of T holds ( A in G iff ex B being Subset of T st ( A = Int B & B in F ) ) ) implies H = G ) assume A1: for A being Subset of T holds ( A in H iff ex B being Subset of T st ( A = Int B & B in F ) ) ; ::_thesis: ( ex A being Subset of T st ( ( A in G implies ex B being Subset of T st ( A = Int B & B in F ) ) implies ( ex B being Subset of T st ( A = Int B & B in F ) & not A in G ) ) or H = G ) assume A2: for A being Subset of T holds ( A in G iff ex B being Subset of T st ( A = Int B & B in F ) ) ; ::_thesis: H = G now__::_thesis:_for_A_being_set_st_A_in_G_holds_ A_in_H let A be set ; ::_thesis: ( A in G implies A in H ) assume A3: A in G ; ::_thesis: A in H then reconsider A0 = A as Subset of T ; ex B being Subset of T st ( A0 = Int B & B in F ) by A2, A3; hence A in H by A1; ::_thesis: verum end; then A4: G c= H by TARSKI:def_3; now__::_thesis:_for_A_being_set_st_A_in_H_holds_ A_in_G let A be set ; ::_thesis: ( A in H implies A in G ) assume A5: A in H ; ::_thesis: A in G then reconsider A0 = A as Subset of T ; ex B being Subset of T st ( A0 = Int B & B in F ) by A1, A5; hence A in G by A2; ::_thesis: verum end; then H c= G by TARSKI:def_3; hence H = G by A4, XBOOLE_0:def_10; ::_thesis: verum end; projectivity for b1, b2 being Subset-Family of T st ( for A being Subset of T holds ( A in b1 iff ex B being Subset of T st ( A = Int B & B in b2 ) ) ) holds for A being Subset of T holds ( A in b1 iff ex B being Subset of T st ( A = Int B & B in b1 ) ) proof let G, F be Subset-Family of T; ::_thesis: ( ( for A being Subset of T holds ( A in G iff ex B being Subset of T st ( A = Int B & B in F ) ) ) implies for A being Subset of T holds ( A in G iff ex B being Subset of T st ( A = Int B & B in G ) ) ) assume A6: for A being Subset of T holds ( A in G iff ex B being Subset of T st ( A = Int B & B in F ) ) ; ::_thesis: for A being Subset of T holds ( A in G iff ex B being Subset of T st ( A = Int B & B in G ) ) let A be Subset of T; ::_thesis: ( A in G iff ex B being Subset of T st ( A = Int B & B in G ) ) thus ( A in G implies ex B being Subset of T st ( A = Int B & B in G ) ) ::_thesis: ( ex B being Subset of T st ( A = Int B & B in G ) implies A in G ) proof assume A in G ; ::_thesis: ex B being Subset of T st ( A = Int B & B in G ) then consider B being Subset of T such that A7: A = Int B and A8: B in F by A6; take C = Int B; ::_thesis: ( A = Int C & C in G ) thus A = Int C by A7; ::_thesis: C in G thus C in G by A8, A6; ::_thesis: verum end; given B being Subset of T such that A9: A = Int B and A10: B in G ; ::_thesis: A in G consider C being Subset of T such that A11: B = Int C and C in F by A10, A6; A = B by A9, A11; hence A in G by A10; ::_thesis: verum end; end; :: deftheorem Def1 defines Int TDLAT_2:def_1_:_ for T being TopSpace for F, b3 being Subset-Family of T holds ( b3 = Int F iff for A being Subset of T holds ( A in b3 iff ex B being Subset of T st ( A = Int B & B in F ) ) ); theorem Th16: :: TDLAT_2:16 for T being TopSpace for F being Subset-Family of T holds Int F = { A where A is Subset of T : ex B being Subset of T st ( A = Int B & B in F ) } proof let T be TopSpace; ::_thesis: for F being Subset-Family of T holds Int F = { A where A is Subset of T : ex B being Subset of T st ( A = Int B & B in F ) } let F be Subset-Family of T; ::_thesis: Int F = { A where A is Subset of T : ex B being Subset of T st ( A = Int B & B in F ) } set P = { A where A is Subset of T : ex B being Subset of T st ( A = Int B & B in F ) } ; now__::_thesis:_for_C_being_set_st_C_in__{__A_where_A_is_Subset_of_T_:_ex_B_being_Subset_of_T_st_ (_A_=_Int_B_&_B_in_F_)__}__holds_ C_in_bool_the_carrier_of_T let C be set ; ::_thesis: ( C in { A where A is Subset of T : ex B being Subset of T st ( A = Int B & B in F ) } implies C in bool the carrier of T ) assume C in { A where A is Subset of T : ex B being Subset of T st ( A = Int B & B in F ) } ; ::_thesis: C in bool the carrier of T then ex A being Subset of T st ( C = A & ex B being Subset of T st ( A = Int B & B in F ) ) ; hence C in bool the carrier of T ; ::_thesis: verum end; then reconsider P = { A where A is Subset of T : ex B being Subset of T st ( A = Int B & B in F ) } as Subset-Family of T by TARSKI:def_3; reconsider P = P as Subset-Family of T ; for X being set holds ( X in Int F iff X in P ) proof let X be set ; ::_thesis: ( X in Int F iff X in P ) A1: now__::_thesis:_(_X_in_P_implies_X_in_Int_F_) assume A2: X in P ; ::_thesis: X in Int F then reconsider C = X as Subset of T ; ex D being Subset of T st ( D = C & ex B being Subset of T st ( D = Int B & B in F ) ) by A2; hence X in Int F by Def1; ::_thesis: verum end; now__::_thesis:_(_X_in_Int_F_implies_X_in_P_) assume A3: X in Int F ; ::_thesis: X in P then reconsider C = X as Subset of T ; ex B being Subset of T st ( C = Int B & B in F ) by A3, Def1; hence X in P ; ::_thesis: verum end; hence ( X in Int F iff X in P ) by A1; ::_thesis: verum end; hence Int F = { A where A is Subset of T : ex B being Subset of T st ( A = Int B & B in F ) } by TARSKI:1; ::_thesis: verum end; theorem :: TDLAT_2:17 canceled; theorem Th18: :: TDLAT_2:18 for T being TopSpace for F being Subset-Family of T holds Int F is open proof let T be TopSpace; ::_thesis: for F being Subset-Family of T holds Int F is open let F be Subset-Family of T; ::_thesis: Int F is open now__::_thesis:_for_A_being_Subset_of_T_st_A_in_Int_F_holds_ A_is_open let A be Subset of T; ::_thesis: ( A in Int F implies A is open ) assume A in Int F ; ::_thesis: A is open then ex B being Subset of T st ( A = Int B & B in F ) by Def1; hence A is open ; ::_thesis: verum end; hence Int F is open by TOPS_2:def_1; ::_thesis: verum end; theorem Th19: :: TDLAT_2:19 for T being TopSpace for F being Subset-Family of T holds ( F = {} iff Int F = {} ) proof let T be TopSpace; ::_thesis: for F being Subset-Family of T holds ( F = {} iff Int F = {} ) let F be Subset-Family of T; ::_thesis: ( F = {} iff Int F = {} ) thus ( F = {} implies Int F = {} ) ::_thesis: ( Int F = {} implies F = {} ) proof set A = the Element of Int F; assume A1: F = {} ; ::_thesis: Int F = {} assume A2: not Int F = {} ; ::_thesis: contradiction then reconsider A = the Element of Int F as Subset of T by TARSKI:def_3; ex V being Subset of T st ( A = Int V & V in F ) by A2, Def1; hence contradiction by A1; ::_thesis: verum end; thus ( Int F = {} implies F = {} ) ::_thesis: verum proof set B = the Element of F; assume A3: Int F = {} ; ::_thesis: F = {} assume A4: not F = {} ; ::_thesis: contradiction then reconsider B = the Element of F as Subset of T by TARSKI:def_3; reconsider A = Int B as set ; ex A being set st A in Int F proof take A ; ::_thesis: A in Int F thus A in Int F by A4, Def1; ::_thesis: verum end; hence contradiction by A3; ::_thesis: verum end; end; theorem Th20: :: TDLAT_2:20 for T being TopSpace for A being Subset of T for F being Subset-Family of T st F = {A} holds Int F = {(Int A)} proof let T be TopSpace; ::_thesis: for A being Subset of T for F being Subset-Family of T st F = {A} holds Int F = {(Int A)} let A be Subset of T; ::_thesis: for F being Subset-Family of T st F = {A} holds Int F = {(Int A)} let F be Subset-Family of T; ::_thesis: ( F = {A} implies Int F = {(Int A)} ) reconsider C = Int F as set ; assume A1: F = {A} ; ::_thesis: Int F = {(Int A)} for B being set holds ( B in C iff B = Int A ) proof let B be set ; ::_thesis: ( B in C iff B = Int A ) A2: now__::_thesis:_(_B_=_Int_A_implies_B_in_C_) assume A3: B = Int A ; ::_thesis: B in C ex M being Subset of T st ( B = Int M & M in F ) proof take A ; ::_thesis: ( B = Int A & A in F ) thus ( B = Int A & A in F ) by A1, A3, TARSKI:def_1; ::_thesis: verum end; hence B in C by Def1; ::_thesis: verum end; now__::_thesis:_(_B_in_C_implies_B_=_Int_A_) assume A4: B in C ; ::_thesis: B = Int A then reconsider B0 = B as Subset of T ; ex M being Subset of T st ( B0 = Int M & M in F ) by A4, Def1; hence B = Int A by A1, TARSKI:def_1; ::_thesis: verum end; hence ( B in C iff B = Int A ) by A2; ::_thesis: verum end; hence Int F = {(Int A)} by TARSKI:def_1; ::_thesis: verum end; theorem :: TDLAT_2:21 for T being TopSpace for F, G being Subset-Family of T st F c= G holds Int F c= Int G proof let T be TopSpace; ::_thesis: for F, G being Subset-Family of T st F c= G holds Int F c= Int G let F, G be Subset-Family of T; ::_thesis: ( F c= G implies Int F c= Int G ) reconsider F0 = Int F, G0 = Int G as set ; assume A1: F c= G ; ::_thesis: Int F c= Int G now__::_thesis:_for_X_being_set_st_X_in_F0_holds_ X_in_G0 let X be set ; ::_thesis: ( X in F0 implies X in G0 ) assume A2: X in F0 ; ::_thesis: X in G0 then reconsider X0 = X as Subset of T ; ex V being Subset of T st ( X0 = Int V & V in F ) by A2, Def1; hence X in G0 by A1, Def1; ::_thesis: verum end; hence Int F c= Int G by TARSKI:def_3; ::_thesis: verum end; theorem Th22: :: TDLAT_2:22 for T being TopSpace for F, G being Subset-Family of T holds Int (F \/ G) = (Int F) \/ (Int G) proof let T be TopSpace; ::_thesis: for F, G being Subset-Family of T holds Int (F \/ G) = (Int F) \/ (Int G) let F, G be Subset-Family of T; ::_thesis: Int (F \/ G) = (Int F) \/ (Int G) for X being set holds ( X in Int (F \/ G) iff X in (Int F) \/ (Int G) ) proof let X be set ; ::_thesis: ( X in Int (F \/ G) iff X in (Int F) \/ (Int G) ) A1: now__::_thesis:_(_X_in_(Int_F)_\/_(Int_G)_implies_X_in_Int_(F_\/_G)_) assume A2: X in (Int F) \/ (Int G) ; ::_thesis: X in Int (F \/ G) now__::_thesis:_X_in_Int_(F_\/_G) percases ( X in Int F or X in Int G ) by A2, XBOOLE_0:def_3; supposeA3: X in Int F ; ::_thesis: X in Int (F \/ G) then reconsider X0 = X as Subset of T ; ex W being Subset of T st ( X0 = Int W & W in F \/ G ) proof consider Z being Subset of T such that A4: X0 = Int Z and A5: Z in F by A3, Def1; take Z ; ::_thesis: ( X0 = Int Z & Z in F \/ G ) thus ( X0 = Int Z & Z in F \/ G ) by A4, A5, XBOOLE_0:def_3; ::_thesis: verum end; hence X in Int (F \/ G) by Def1; ::_thesis: verum end; supposeA6: X in Int G ; ::_thesis: X in Int (F \/ G) then reconsider X0 = X as Subset of T ; ex W being Subset of T st ( X0 = Int W & W in F \/ G ) proof consider Z being Subset of T such that A7: X0 = Int Z and A8: Z in G by A6, Def1; take Z ; ::_thesis: ( X0 = Int Z & Z in F \/ G ) thus ( X0 = Int Z & Z in F \/ G ) by A7, A8, XBOOLE_0:def_3; ::_thesis: verum end; hence X in Int (F \/ G) by Def1; ::_thesis: verum end; end; end; hence X in Int (F \/ G) ; ::_thesis: verum end; now__::_thesis:_(_X_in_Int_(F_\/_G)_implies_X_in_(Int_F)_\/_(Int_G)_) assume A9: X in Int (F \/ G) ; ::_thesis: X in (Int F) \/ (Int G) then reconsider X0 = X as Subset of T ; consider W being Subset of T such that A10: X0 = Int W and A11: W in F \/ G by A9, Def1; now__::_thesis:_X0_in_(Int_F)_\/_(Int_G) percases ( W in F or W in G ) by A11, XBOOLE_0:def_3; suppose W in F ; ::_thesis: X0 in (Int F) \/ (Int G) then X0 in Int F by A10, Def1; hence X0 in (Int F) \/ (Int G) by XBOOLE_0:def_3; ::_thesis: verum end; suppose W in G ; ::_thesis: X0 in (Int F) \/ (Int G) then X0 in Int G by A10, Def1; hence X0 in (Int F) \/ (Int G) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence X in (Int F) \/ (Int G) ; ::_thesis: verum end; hence ( X in Int (F \/ G) iff X in (Int F) \/ (Int G) ) by A1; ::_thesis: verum end; hence Int (F \/ G) = (Int F) \/ (Int G) by TARSKI:1; ::_thesis: verum end; theorem :: TDLAT_2:23 for T being TopSpace for F, G being Subset-Family of T holds Int (F /\ G) c= (Int F) /\ (Int G) proof let T be TopSpace; ::_thesis: for F, G being Subset-Family of T holds Int (F /\ G) c= (Int F) /\ (Int G) let F, G be Subset-Family of T; ::_thesis: Int (F /\ G) c= (Int F) /\ (Int G) for X being set st X in Int (F /\ G) holds X in (Int F) /\ (Int G) proof let X be set ; ::_thesis: ( X in Int (F /\ G) implies X in (Int F) /\ (Int G) ) assume A1: X in Int (F /\ G) ; ::_thesis: X in (Int F) /\ (Int G) then reconsider X0 = X as Subset of T ; consider W being Subset of T such that A2: X0 = Int W and A3: W in F /\ G by A1, Def1; W in G by A3, XBOOLE_0:def_4; then A4: X0 in Int G by A2, Def1; W in F by A3, XBOOLE_0:def_4; then X0 in Int F by A2, Def1; hence X in (Int F) /\ (Int G) by A4, XBOOLE_0:def_4; ::_thesis: verum end; hence Int (F /\ G) c= (Int F) /\ (Int G) by TARSKI:def_3; ::_thesis: verum end; theorem :: TDLAT_2:24 for T being TopSpace for F, G being Subset-Family of T holds (Int F) \ (Int G) c= Int (F \ G) proof let T be TopSpace; ::_thesis: for F, G being Subset-Family of T holds (Int F) \ (Int G) c= Int (F \ G) let F, G be Subset-Family of T; ::_thesis: (Int F) \ (Int G) c= Int (F \ G) for X being set st X in (Int F) \ (Int G) holds X in Int (F \ G) proof let X be set ; ::_thesis: ( X in (Int F) \ (Int G) implies X in Int (F \ G) ) assume A1: X in (Int F) \ (Int G) ; ::_thesis: X in Int (F \ G) then reconsider X0 = X as Subset of T ; X in Int F by A1, XBOOLE_0:def_5; then consider W being Subset of T such that A2: X0 = Int W and A3: W in F by Def1; not X in Int G by A1, XBOOLE_0:def_5; then not W in G by A2, Def1; then W in F \ G by A3, XBOOLE_0:def_5; hence X in Int (F \ G) by A2, Def1; ::_thesis: verum end; hence (Int F) \ (Int G) c= Int (F \ G) by TARSKI:def_3; ::_thesis: verum end; theorem :: TDLAT_2:25 for T being TopSpace for F being Subset-Family of T for A being Subset of T st A in F holds ( Int A c= union (Int F) & meet (Int F) c= Int A ) proof let T be TopSpace; ::_thesis: for F being Subset-Family of T for A being Subset of T st A in F holds ( Int A c= union (Int F) & meet (Int F) c= Int A ) let F be Subset-Family of T; ::_thesis: for A being Subset of T st A in F holds ( Int A c= union (Int F) & meet (Int F) c= Int A ) let A be Subset of T; ::_thesis: ( A in F implies ( Int A c= union (Int F) & meet (Int F) c= Int A ) ) assume A in F ; ::_thesis: ( Int A c= union (Int F) & meet (Int F) c= Int A ) then Int A in { P where P is Subset of T : ex B being Subset of T st ( P = Int B & B in F ) } ; then A1: Int A in Int F by Th16; hence Int A c= union (Int F) by ZFMISC_1:74; ::_thesis: meet (Int F) c= Int A thus meet (Int F) c= Int A by A1, SETFAM_1:3; ::_thesis: verum end; theorem Th26: :: TDLAT_2:26 for T being TopSpace for F being Subset-Family of T holds union (Int F) c= union F proof let T be TopSpace; ::_thesis: for F being Subset-Family of T holds union (Int F) c= union F let F be Subset-Family of T; ::_thesis: union (Int F) c= union F now__::_thesis:_for_x_being_set_st_x_in_union_(Int_F)_holds_ x_in_union_F let x be set ; ::_thesis: ( x in union (Int F) implies x in union F ) assume x in union (Int F) ; ::_thesis: x in union F then consider A being set such that A1: x in A and A2: A in Int F by TARSKI:def_4; reconsider A = A as Subset of T by A2; consider B being Subset of T such that A3: A = Int B and A4: B in F by A2, Def1; ex B being set st ( x in B & B in F ) proof take B ; ::_thesis: ( x in B & B in F ) Int B c= B by TOPS_1:16; hence ( x in B & B in F ) by A1, A3, A4; ::_thesis: verum end; hence x in union F by TARSKI:def_4; ::_thesis: verum end; hence union (Int F) c= union F by TARSKI:def_3; ::_thesis: verum end; theorem :: TDLAT_2:27 for T being TopSpace for F being Subset-Family of T holds meet (Int F) c= meet F proof let T be TopSpace; ::_thesis: for F being Subset-Family of T holds meet (Int F) c= meet F let F be Subset-Family of T; ::_thesis: meet (Int F) c= meet F A1: for A being set st A in F holds meet (Int F) c= A proof let A be set ; ::_thesis: ( A in F implies meet (Int F) c= A ) assume A2: A in F ; ::_thesis: meet (Int F) c= A then reconsider A0 = A as Subset of T ; set C = Int A0; Int A0 in { P where P is Subset of T : ex Q being Subset of T st ( P = Int Q & Q in F ) } by A2; then Int A0 in Int F by Th16; then A3: meet (Int F) c= Int A0 by SETFAM_1:3; Int A0 c= A0 by TOPS_1:16; hence meet (Int F) c= A by A3, XBOOLE_1:1; ::_thesis: verum end; now__::_thesis:_meet_(Int_F)_c=_meet_F percases ( F = {} or F <> {} ) ; suppose F = {} ; ::_thesis: meet (Int F) c= meet F hence meet (Int F) c= meet F by Th19; ::_thesis: verum end; suppose F <> {} ; ::_thesis: meet (Int F) c= meet F hence meet (Int F) c= meet F by A1, SETFAM_1:5; ::_thesis: verum end; end; end; hence meet (Int F) c= meet F ; ::_thesis: verum end; theorem Th28: :: TDLAT_2:28 for T being TopSpace for F being Subset-Family of T holds union (Int F) c= Int (union F) proof let T be TopSpace; ::_thesis: for F being Subset-Family of T holds union (Int F) c= Int (union F) let F be Subset-Family of T; ::_thesis: union (Int F) c= Int (union F) A1: Int (union (Int F)) c= Int (union F) by Th26, TOPS_1:19; union (Int F) is open by Th18, TOPS_2:19; hence union (Int F) c= Int (union F) by A1, TOPS_1:23; ::_thesis: verum end; theorem Th29: :: TDLAT_2:29 for T being TopSpace for F being Subset-Family of T holds Int (meet F) c= meet (Int F) proof let T be TopSpace; ::_thesis: for F being Subset-Family of T holds Int (meet F) c= meet (Int F) let F be Subset-Family of T; ::_thesis: Int (meet F) c= meet (Int F) A1: for A being set st A in Int F holds Int (meet F) c= A proof let A be set ; ::_thesis: ( A in Int F implies Int (meet F) c= A ) assume A2: A in Int F ; ::_thesis: Int (meet F) c= A then reconsider A0 = A as Subset of T ; A0 in { B where B is Subset of T : ex C being Subset of T st ( B = Int C & C in F ) } by A2, Th16; then ex P being Subset of T st ( P = A0 & ex C being Subset of T st ( P = Int C & C in F ) ) ; hence Int (meet F) c= A by SETFAM_1:3, TOPS_1:19; ::_thesis: verum end; now__::_thesis:_Int_(meet_F)_c=_meet_(Int_F) percases ( Int F = {} or Int F <> {} ) ; supposeA3: Int F = {} ; ::_thesis: Int (meet F) c= meet (Int F) then meet F = {} T by Th19, SETFAM_1:1; hence Int (meet F) c= meet (Int F) by A3, SETFAM_1:1; ::_thesis: verum end; suppose Int F <> {} ; ::_thesis: Int (meet F) c= meet (Int F) hence Int (meet F) c= meet (Int F) by A1, SETFAM_1:5; ::_thesis: verum end; end; end; hence Int (meet F) c= meet (Int F) ; ::_thesis: verum end; theorem :: TDLAT_2:30 for T being TopSpace for F being Subset-Family of T st F is finite holds Int (meet F) = meet (Int F) proof let T be TopSpace; ::_thesis: for F being Subset-Family of T st F is finite holds Int (meet F) = meet (Int F) let F be Subset-Family of T; ::_thesis: ( F is finite implies Int (meet F) = meet (Int F) ) assume A1: F is finite ; ::_thesis: Int (meet F) = meet (Int F) A2: meet (Int F) c= Int (meet F) proof consider p being FinSequence such that A3: rng p = F by A1, FINSEQ_1:52; consider n being Nat such that A4: dom p = Seg n by FINSEQ_1:def_2; defpred S1[ Nat] means for G being Subset-Family of T st G = p .: (Seg \$1) & \$1 <= n & 1 <= n holds meet (Int G) c= Int (meet G); A5: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A6: for G being Subset-Family of T st G = p .: (Seg k) & k <= n & 1 <= n holds meet (Int G) c= Int (meet G) ; ::_thesis: S1[k + 1] let G be Subset-Family of T; ::_thesis: ( G = p .: (Seg (k + 1)) & k + 1 <= n & 1 <= n implies meet (Int G) c= Int (meet G) ) assume A7: G = p .: (Seg (k + 1)) ; ::_thesis: ( not k + 1 <= n or not 1 <= n or meet (Int G) c= Int (meet G) ) assume that A8: k + 1 <= n and A9: 1 <= n ; ::_thesis: meet (Int G) c= Int (meet G) A10: now__::_thesis:_(_0_<_k_implies_meet_(Int_G)_c=_Int_(meet_G)_) reconsider G2 = Im (p,(k + 1)) as Subset-Family of T by A3, RELAT_1:111, TOPS_2:2; reconsider G1 = p .: (Seg k) as Subset-Family of T by A3, RELAT_1:111, TOPS_2:2; A11: 0 + 1 = 1 ; 0 <= k by NAT_1:2; then 1 <= k + 1 by A11, XREAL_1:7; then A12: k + 1 in dom p by A4, A8, FINSEQ_1:1; then A13: G2 = {(p . (k + 1))} by FUNCT_1:59; then meet G2 = p . (k + 1) by SETFAM_1:10; then reconsider G3 = p . (k + 1) as Subset of T ; A14: meet (Int G2) = meet {(Int G3)} by A13, Th20 .= Int G3 by SETFAM_1:10 .= Int (meet G2) by A13, SETFAM_1:10 ; k + 1 <= n + 1 by A8, NAT_1:12; then k <= n by XREAL_1:6; then A15: meet (Int G1) c= Int (meet G1) by A6, A9; assume 0 < k ; ::_thesis: meet (Int G) c= Int (meet G) then A16: 0 + 1 <= k by NAT_1:13; then A17: k in Seg k by FINSEQ_1:1; k <= n by A8, NAT_1:13; then k in dom p by A4, A16, FINSEQ_1:1; then A18: p . k in G1 by A17, FUNCT_1:def_6; k + 1 in {(k + 1)} by TARSKI:def_1; then A19: p . (k + 1) in G2 by A12, FUNCT_1:def_6; then A20: Int G2 <> {} by Th19; A21: p .: (Seg (k + 1)) = p .: ((Seg k) \/ {(k + 1)}) by FINSEQ_1:9 .= (p .: (Seg k)) \/ (p .: {(k + 1)}) by RELAT_1:120 ; then Int (meet G) = Int ((meet G1) /\ (meet G2)) by A7, A18, A19, SETFAM_1:9 .= (Int (meet G1)) /\ (Int (meet G2)) by TOPS_1:17 ; then A22: (meet (Int G1)) /\ (meet (Int G2)) c= Int (meet G) by A14, A15, XBOOLE_1:27; Int G1 <> {} by A18, Th19; then meet ((Int G1) \/ (Int G2)) c= Int (meet G) by A20, A22, SETFAM_1:9; hence meet (Int G) c= Int (meet G) by A7, A21, Th22; ::_thesis: verum end; now__::_thesis:_(_k_=_0_implies_meet_(Int_G)_c=_Int_(meet_G)_) assume A23: k = 0 ; ::_thesis: meet (Int G) c= Int (meet G) then 1 in dom p by A4, A8, FINSEQ_1:1; then A24: Im (p,1) = {(p . 1)} by FUNCT_1:59; then union G = p . 1 by A7, A23, FINSEQ_1:2, ZFMISC_1:25; then reconsider G1 = p . 1 as Subset of T ; Int (meet G) = Int G1 by A7, A23, A24, FINSEQ_1:2, SETFAM_1:10 .= meet {(Int G1)} by SETFAM_1:10 .= meet (Int G) by A7, A23, A24, Th20, FINSEQ_1:2 ; hence meet (Int G) c= Int (meet G) ; ::_thesis: verum end; hence meet (Int G) c= Int (meet G) by A10, NAT_1:3; ::_thesis: verum end; A25: S1[ 0 ] by Th19, SETFAM_1:1; A27: for k being Nat holds S1[k] from NAT_1:sch_2(A25, A5); A28: now__::_thesis:_(_1_<=_n_implies_meet_(Int_F)_c=_Int_(meet_F)_) assume A29: 1 <= n ; ::_thesis: meet (Int F) c= Int (meet F) F = p .: (Seg n) by A3, A4, RELAT_1:113; hence meet (Int F) c= Int (meet F) by A27, A29; ::_thesis: verum end; A30: now__::_thesis:_(_n_<>_0_implies_1_<=_n_) assume n <> 0 ; ::_thesis: 1 <= n then A31: 0 < n by NAT_1:3; 1 = 0 + 1 ; hence 1 <= n by A31, NAT_1:13; ::_thesis: verum end; now__::_thesis:_(_n_=_0_implies_meet_(Int_F)_c=_Int_(meet_F)_) assume n = 0 ; ::_thesis: meet (Int F) c= Int (meet F) then Seg n = {} ; then F = p .: {} by A3, A4, RELAT_1:113; then F = {} ; hence meet (Int F) c= Int (meet F) by Th19, SETFAM_1:1; ::_thesis: verum end; hence meet (Int F) c= Int (meet F) by A28, A30; ::_thesis: verum end; Int (meet F) c= meet (Int F) by Th29; hence Int (meet F) = meet (Int F) by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th31: :: TDLAT_2:31 for T being non empty TopSpace for F being Subset-Family of T holds Cl (Int F) = { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int B) & B in F ) } proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Cl (Int F) = { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int B) & B in F ) } let F be Subset-Family of T; ::_thesis: Cl (Int F) = { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int B) & B in F ) } set P = { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int B) & B in F ) } ; now__::_thesis:_for_C_being_set_st_C_in__{__A_where_A_is_Subset_of_T_:_ex_B_being_Subset_of_T_st_ (_A_=_Cl_(Int_B)_&_B_in_F_)__}__holds_ C_in_bool_the_carrier_of_T let C be set ; ::_thesis: ( C in { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int B) & B in F ) } implies C in bool the carrier of T ) assume C in { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int B) & B in F ) } ; ::_thesis: C in bool the carrier of T then ex A being Subset of T st ( C = A & ex B being Subset of T st ( A = Cl (Int B) & B in F ) ) ; hence C in bool the carrier of T ; ::_thesis: verum end; then reconsider P = { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int B) & B in F ) } as Subset-Family of T by TARSKI:def_3; reconsider P = P as Subset-Family of T ; for X being set holds ( X in Cl (Int F) iff X in P ) proof let X be set ; ::_thesis: ( X in Cl (Int F) iff X in P ) A1: now__::_thesis:_(_X_in_P_implies_X_in_Cl_(Int_F)_) assume A2: X in P ; ::_thesis: X in Cl (Int F) then reconsider C = X as Subset of T ; ex D being Subset of T st ( D = C & ex B being Subset of T st ( D = Cl (Int B) & B in F ) ) by A2; then consider B being Subset of T such that A3: C = Cl (Int B) and A4: B in F ; Int B in Int F by A4, Def1; hence X in Cl (Int F) by A3, PCOMPS_1:def_2; ::_thesis: verum end; now__::_thesis:_(_X_in_Cl_(Int_F)_implies_X_in_P_) assume A5: X in Cl (Int F) ; ::_thesis: X in P then reconsider C = X as Subset of T ; consider B being Subset of T such that A6: C = Cl B and A7: B in Int F by A5, PCOMPS_1:def_2; ex D being Subset of T st ( B = Int D & D in F ) by A7, Def1; hence X in P by A6; ::_thesis: verum end; hence ( X in Cl (Int F) iff X in P ) by A1; ::_thesis: verum end; hence Cl (Int F) = { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int B) & B in F ) } by TARSKI:1; ::_thesis: verum end; theorem Th32: :: TDLAT_2:32 for T being non empty TopSpace for F being Subset-Family of T holds Int (Cl F) = { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl B) & B in F ) } proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Int (Cl F) = { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl B) & B in F ) } let F be Subset-Family of T; ::_thesis: Int (Cl F) = { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl B) & B in F ) } set P = { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl B) & B in F ) } ; now__::_thesis:_for_C_being_set_st_C_in__{__A_where_A_is_Subset_of_T_:_ex_B_being_Subset_of_T_st_ (_A_=_Int_(Cl_B)_&_B_in_F_)__}__holds_ C_in_bool_the_carrier_of_T let C be set ; ::_thesis: ( C in { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl B) & B in F ) } implies C in bool the carrier of T ) assume C in { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl B) & B in F ) } ; ::_thesis: C in bool the carrier of T then ex A being Subset of T st ( C = A & ex B being Subset of T st ( A = Int (Cl B) & B in F ) ) ; hence C in bool the carrier of T ; ::_thesis: verum end; then reconsider P = { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl B) & B in F ) } as Subset-Family of T by TARSKI:def_3; reconsider P = P as Subset-Family of T ; for X being set holds ( X in Int (Cl F) iff X in P ) proof let X be set ; ::_thesis: ( X in Int (Cl F) iff X in P ) A1: now__::_thesis:_(_X_in_P_implies_X_in_Int_(Cl_F)_) assume A2: X in P ; ::_thesis: X in Int (Cl F) then reconsider C = X as Subset of T ; ex D being Subset of T st ( D = C & ex B being Subset of T st ( D = Int (Cl B) & B in F ) ) by A2; then consider B being Subset of T such that A3: C = Int (Cl B) and A4: B in F ; Cl B in Cl F by A4, PCOMPS_1:def_2; hence X in Int (Cl F) by A3, Def1; ::_thesis: verum end; now__::_thesis:_(_X_in_Int_(Cl_F)_implies_X_in_P_) assume A5: X in Int (Cl F) ; ::_thesis: X in P then reconsider C = X as Subset of T ; consider B being Subset of T such that A6: C = Int B and A7: B in Cl F by A5, Def1; ex D being Subset of T st ( B = Cl D & D in F ) by A7, PCOMPS_1:def_2; hence X in P by A6; ::_thesis: verum end; hence ( X in Int (Cl F) iff X in P ) by A1; ::_thesis: verum end; hence Int (Cl F) = { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl B) & B in F ) } by TARSKI:1; ::_thesis: verum end; theorem Th33: :: TDLAT_2:33 for T being non empty TopSpace for F being Subset-Family of T holds Cl (Int (Cl F)) = { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int (Cl B)) & B in F ) } proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Cl (Int (Cl F)) = { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int (Cl B)) & B in F ) } let F be Subset-Family of T; ::_thesis: Cl (Int (Cl F)) = { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int (Cl B)) & B in F ) } set P = { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int (Cl B)) & B in F ) } ; now__::_thesis:_for_C_being_set_st_C_in__{__A_where_A_is_Subset_of_T_:_ex_B_being_Subset_of_T_st_ (_A_=_Cl_(Int_(Cl_B))_&_B_in_F_)__}__holds_ C_in_bool_the_carrier_of_T let C be set ; ::_thesis: ( C in { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int (Cl B)) & B in F ) } implies C in bool the carrier of T ) assume C in { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int (Cl B)) & B in F ) } ; ::_thesis: C in bool the carrier of T then ex A being Subset of T st ( C = A & ex B being Subset of T st ( A = Cl (Int (Cl B)) & B in F ) ) ; hence C in bool the carrier of T ; ::_thesis: verum end; then reconsider P = { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int (Cl B)) & B in F ) } as Subset-Family of T by TARSKI:def_3; reconsider P = P as Subset-Family of T ; for X being set holds ( X in Cl (Int (Cl F)) iff X in P ) proof let X be set ; ::_thesis: ( X in Cl (Int (Cl F)) iff X in P ) A1: now__::_thesis:_(_X_in_P_implies_X_in_Cl_(Int_(Cl_F))_) assume A2: X in P ; ::_thesis: X in Cl (Int (Cl F)) then reconsider C = X as Subset of T ; ex D being Subset of T st ( D = C & ex B being Subset of T st ( D = Cl (Int (Cl B)) & B in F ) ) by A2; then consider B being Subset of T such that A3: C = Cl (Int (Cl B)) and A4: B in F ; Cl B in Cl F by A4, PCOMPS_1:def_2; then Int (Cl B) in Int (Cl F) by Def1; hence X in Cl (Int (Cl F)) by A3, PCOMPS_1:def_2; ::_thesis: verum end; now__::_thesis:_(_X_in_Cl_(Int_(Cl_F))_implies_X_in_P_) assume A5: X in Cl (Int (Cl F)) ; ::_thesis: X in P then reconsider C = X as Subset of T ; consider B being Subset of T such that A6: C = Cl B and A7: B in Int (Cl F) by A5, PCOMPS_1:def_2; consider D being Subset of T such that A8: B = Int D and A9: D in Cl F by A7, Def1; ex E being Subset of T st ( D = Cl E & E in F ) by A9, PCOMPS_1:def_2; hence X in P by A6, A8; ::_thesis: verum end; hence ( X in Cl (Int (Cl F)) iff X in P ) by A1; ::_thesis: verum end; hence Cl (Int (Cl F)) = { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int (Cl B)) & B in F ) } by TARSKI:1; ::_thesis: verum end; theorem Th34: :: TDLAT_2:34 for T being non empty TopSpace for F being Subset-Family of T holds Int (Cl (Int F)) = { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl (Int B)) & B in F ) } proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Int (Cl (Int F)) = { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl (Int B)) & B in F ) } let F be Subset-Family of T; ::_thesis: Int (Cl (Int F)) = { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl (Int B)) & B in F ) } set P = { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl (Int B)) & B in F ) } ; now__::_thesis:_for_C_being_set_st_C_in__{__A_where_A_is_Subset_of_T_:_ex_B_being_Subset_of_T_st_ (_A_=_Int_(Cl_(Int_B))_&_B_in_F_)__}__holds_ C_in_bool_the_carrier_of_T let C be set ; ::_thesis: ( C in { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl (Int B)) & B in F ) } implies C in bool the carrier of T ) assume C in { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl (Int B)) & B in F ) } ; ::_thesis: C in bool the carrier of T then ex A being Subset of T st ( C = A & ex B being Subset of T st ( A = Int (Cl (Int B)) & B in F ) ) ; hence C in bool the carrier of T ; ::_thesis: verum end; then reconsider P = { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl (Int B)) & B in F ) } as Subset-Family of T by TARSKI:def_3; reconsider P = P as Subset-Family of T ; for X being set holds ( X in Int (Cl (Int F)) iff X in P ) proof let X be set ; ::_thesis: ( X in Int (Cl (Int F)) iff X in P ) A1: now__::_thesis:_(_X_in_P_implies_X_in_Int_(Cl_(Int_F))_) assume A2: X in P ; ::_thesis: X in Int (Cl (Int F)) then reconsider C = X as Subset of T ; ex D being Subset of T st ( D = C & ex B being Subset of T st ( D = Int (Cl (Int B)) & B in F ) ) by A2; then consider B being Subset of T such that A3: C = Int (Cl (Int B)) and A4: B in F ; Int B in Int F by A4, Def1; then Cl (Int B) in Cl (Int F) by PCOMPS_1:def_2; hence X in Int (Cl (Int F)) by A3, Def1; ::_thesis: verum end; now__::_thesis:_(_X_in_Int_(Cl_(Int_F))_implies_X_in_P_) assume A5: X in Int (Cl (Int F)) ; ::_thesis: X in P then reconsider C = X as Subset of T ; consider B being Subset of T such that A6: C = Int B and A7: B in Cl (Int F) by A5, Def1; consider D being Subset of T such that A8: B = Cl D and A9: D in Int F by A7, PCOMPS_1:def_2; ex E being Subset of T st ( D = Int E & E in F ) by A9, Def1; hence X in P by A6, A8; ::_thesis: verum end; hence ( X in Int (Cl (Int F)) iff X in P ) by A1; ::_thesis: verum end; hence Int (Cl (Int F)) = { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl (Int B)) & B in F ) } by TARSKI:1; ::_thesis: verum end; theorem :: TDLAT_2:35 for T being non empty TopSpace for F being Subset-Family of T holds Cl (Int (Cl (Int F))) = Cl (Int F) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Cl (Int (Cl (Int F))) = Cl (Int F) let F be Subset-Family of T; ::_thesis: Cl (Int (Cl (Int F))) = Cl (Int F) set H = { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl (Int B)) & B in F ) } ; Int (Cl (Int F)) = { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl (Int B)) & B in F ) } by Th34; then reconsider H = { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl (Int B)) & B in F ) } as Subset-Family of T ; A1: Cl (Int (Cl (Int F))) = Cl H by Th34; A2: Cl (Int F) = { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int B) & B in F ) } by Th31; for X being set holds ( X in Cl (Int (Cl (Int F))) iff X in Cl (Int F) ) proof let X be set ; ::_thesis: ( X in Cl (Int (Cl (Int F))) iff X in Cl (Int F) ) A3: now__::_thesis:_(_X_in_Cl_(Int_F)_implies_X_in_Cl_(Int_(Cl_(Int_F)))_) assume A4: X in Cl (Int F) ; ::_thesis: X in Cl (Int (Cl (Int F))) then reconsider C = X as Subset of T ; ex D being Subset of T st ( D = C & ex B being Subset of T st ( D = Cl (Int B) & B in F ) ) by A2, A4; then consider B being Subset of T such that A5: C = Cl (Int B) and A6: B in F ; Int B in Int F by A6, Def1; then Cl (Int B) in Cl (Int F) by PCOMPS_1:def_2; then A7: Int (Cl (Int B)) in Int (Cl (Int F)) by Def1; C = Cl (Int (Cl (Int B))) by A5, TOPS_1:26; hence X in Cl (Int (Cl (Int F))) by A7, PCOMPS_1:def_2; ::_thesis: verum end; now__::_thesis:_(_X_in_Cl_(Int_(Cl_(Int_F)))_implies_X_in_Cl_(Int_F)_) assume A8: X in Cl (Int (Cl (Int F))) ; ::_thesis: X in Cl (Int F) then reconsider C = X as Subset of T ; consider B being Subset of T such that A9: C = Cl B and A10: B in { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl (Int B)) & B in F ) } by A1, A8, PCOMPS_1:def_2; ex S being Subset of T st ( S = B & ex R being Subset of T st ( S = Int (Cl (Int R)) & R in F ) ) by A10; then consider D being Subset of T such that A11: B = Int (Cl (Int D)) and A12: D in F ; A13: Int D in Int F by A12, Def1; C = Cl (Int D) by A9, A11, TOPS_1:26; hence X in Cl (Int F) by A13, PCOMPS_1:def_2; ::_thesis: verum end; hence ( X in Cl (Int (Cl (Int F))) iff X in Cl (Int F) ) by A3; ::_thesis: verum end; hence Cl (Int (Cl (Int F))) = Cl (Int F) by TARSKI:1; ::_thesis: verum end; theorem :: TDLAT_2:36 for T being non empty TopSpace for F being Subset-Family of T holds Int (Cl (Int (Cl F))) = Int (Cl F) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Int (Cl (Int (Cl F))) = Int (Cl F) let F be Subset-Family of T; ::_thesis: Int (Cl (Int (Cl F))) = Int (Cl F) set H = { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int (Cl B)) & B in F ) } ; Cl (Int (Cl F)) = { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int (Cl B)) & B in F ) } by Th33; then reconsider H = { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int (Cl B)) & B in F ) } as Subset-Family of T ; A1: Int (Cl (Int (Cl F))) = Int H by Th33; A2: Int (Cl F) = { A where A is Subset of T : ex B being Subset of T st ( A = Int (Cl B) & B in F ) } by Th32; for X being set holds ( X in Int (Cl (Int (Cl F))) iff X in Int (Cl F) ) proof let X be set ; ::_thesis: ( X in Int (Cl (Int (Cl F))) iff X in Int (Cl F) ) A3: now__::_thesis:_(_X_in_Int_(Cl_F)_implies_X_in_Int_(Cl_(Int_(Cl_F)))_) assume A4: X in Int (Cl F) ; ::_thesis: X in Int (Cl (Int (Cl F))) then reconsider C = X as Subset of T ; ex D being Subset of T st ( D = C & ex B being Subset of T st ( D = Int (Cl B) & B in F ) ) by A2, A4; then consider B being Subset of T such that A5: C = Int (Cl B) and A6: B in F ; Cl B in Cl F by A6, PCOMPS_1:def_2; then Int (Cl B) in Int (Cl F) by Def1; then A7: Cl (Int (Cl B)) in Cl (Int (Cl F)) by PCOMPS_1:def_2; C = Int (Cl (Int (Cl B))) by A5, TDLAT_1:5; hence X in Int (Cl (Int (Cl F))) by A7, Def1; ::_thesis: verum end; now__::_thesis:_(_X_in_Int_(Cl_(Int_(Cl_F)))_implies_X_in_Int_(Cl_F)_) assume A8: X in Int (Cl (Int (Cl F))) ; ::_thesis: X in Int (Cl F) then reconsider C = X as Subset of T ; consider B being Subset of T such that A9: C = Int B and A10: B in { A where A is Subset of T : ex B being Subset of T st ( A = Cl (Int (Cl B)) & B in F ) } by A1, A8, Def1; ex S being Subset of T st ( S = B & ex R being Subset of T st ( S = Cl (Int (Cl R)) & R in F ) ) by A10; then consider D being Subset of T such that A11: B = Cl (Int (Cl D)) and A12: D in F ; A13: Cl D in Cl F by A12, PCOMPS_1:def_2; C = Int (Cl D) by A9, A11, TDLAT_1:5; hence X in Int (Cl F) by A13, Def1; ::_thesis: verum end; hence ( X in Int (Cl (Int (Cl F))) iff X in Int (Cl F) ) by A3; ::_thesis: verum end; hence Int (Cl (Int (Cl F))) = Int (Cl F) by TARSKI:1; ::_thesis: verum end; theorem :: TDLAT_2:37 for T being non empty TopSpace for F being Subset-Family of T holds union (Int (Cl F)) c= union (Cl (Int (Cl F))) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Int (Cl F)) c= union (Cl (Int (Cl F))) let F be Subset-Family of T; ::_thesis: union (Int (Cl F)) c= union (Cl (Int (Cl F))) now__::_thesis:_for_x_being_set_st_x_in_union_(Int_(Cl_F))_holds_ x_in_union_(Cl_(Int_(Cl_F))) let x be set ; ::_thesis: ( x in union (Int (Cl F)) implies x in union (Cl (Int (Cl F))) ) assume x in union (Int (Cl F)) ; ::_thesis: x in union (Cl (Int (Cl F))) then consider A being set such that A1: x in A and A2: A in Int (Cl F) by TARSKI:def_4; reconsider A = A as Subset of T by A2; consider B being Subset of T such that A3: A = Int B and A4: B in Cl F by A2, Def1; consider D being Subset of T such that A5: B = Cl D and A6: D in F by A4, PCOMPS_1:def_2; ex P being set st ( x in P & P in Cl (Int (Cl F)) ) proof take Cl (Int (Cl D)) ; ::_thesis: ( x in Cl (Int (Cl D)) & Cl (Int (Cl D)) in Cl (Int (Cl F)) ) Cl D in Cl F by A6, PCOMPS_1:def_2; then A7: Int (Cl D) in Int (Cl F) by Def1; A c= Cl (Int (Cl D)) by A3, A5, Th2; hence ( x in Cl (Int (Cl D)) & Cl (Int (Cl D)) in Cl (Int (Cl F)) ) by A1, A7, PCOMPS_1:def_2; ::_thesis: verum end; hence x in union (Cl (Int (Cl F))) by TARSKI:def_4; ::_thesis: verum end; hence union (Int (Cl F)) c= union (Cl (Int (Cl F))) by TARSKI:def_3; ::_thesis: verum end; theorem :: TDLAT_2:38 for T being non empty TopSpace for F being Subset-Family of T holds meet (Int (Cl F)) c= meet (Cl (Int (Cl F))) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds meet (Int (Cl F)) c= meet (Cl (Int (Cl F))) let F be Subset-Family of T; ::_thesis: meet (Int (Cl F)) c= meet (Cl (Int (Cl F))) now__::_thesis:_meet_(Int_(Cl_F))_c=_meet_(Cl_(Int_(Cl_F))) percases ( F = {} or F <> {} ) ; suppose F = {} ; ::_thesis: meet (Int (Cl F)) c= meet (Cl (Int (Cl F))) then Cl F = {} by Th9; then Int (Cl F) = {} by Th19; hence meet (Int (Cl F)) c= meet (Cl (Int (Cl F))) by Th9; ::_thesis: verum end; suppose F <> {} ; ::_thesis: meet (Int (Cl F)) c= meet (Cl (Int (Cl F))) then Cl F <> {} by Th9; then Int (Cl F) <> {} by Th19; then A1: Cl (Int (Cl F)) <> {} by Th9; now__::_thesis:_for_x_being_set_st_x_in_meet_(Int_(Cl_F))_holds_ x_in_meet_(Cl_(Int_(Cl_F))) let x be set ; ::_thesis: ( x in meet (Int (Cl F)) implies x in meet (Cl (Int (Cl F))) ) assume A2: x in meet (Int (Cl F)) ; ::_thesis: x in meet (Cl (Int (Cl F))) for A being set st A in Cl (Int (Cl F)) holds x in A proof let A be set ; ::_thesis: ( A in Cl (Int (Cl F)) implies x in A ) assume A3: A in Cl (Int (Cl F)) ; ::_thesis: x in A then reconsider A = A as Subset of T ; consider B being Subset of T such that A4: A = Cl B and A5: B in Int (Cl F) by A3, PCOMPS_1:def_2; A6: B c= Cl B by PRE_TOPC:18; x in B by A2, A5, SETFAM_1:def_1; hence x in A by A4, A6; ::_thesis: verum end; hence x in meet (Cl (Int (Cl F))) by A1, SETFAM_1:def_1; ::_thesis: verum end; hence meet (Int (Cl F)) c= meet (Cl (Int (Cl F))) by TARSKI:def_3; ::_thesis: verum end; end; end; hence meet (Int (Cl F)) c= meet (Cl (Int (Cl F))) ; ::_thesis: verum end; theorem :: TDLAT_2:39 for T being non empty TopSpace for F being Subset-Family of T holds union (Cl (Int F)) c= union (Cl (Int (Cl F))) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Cl (Int F)) c= union (Cl (Int (Cl F))) let F be Subset-Family of T; ::_thesis: union (Cl (Int F)) c= union (Cl (Int (Cl F))) now__::_thesis:_for_x_being_set_st_x_in_union_(Cl_(Int_F))_holds_ x_in_union_(Cl_(Int_(Cl_F))) let x be set ; ::_thesis: ( x in union (Cl (Int F)) implies x in union (Cl (Int (Cl F))) ) assume x in union (Cl (Int F)) ; ::_thesis: x in union (Cl (Int (Cl F))) then consider A being set such that A1: x in A and A2: A in Cl (Int F) by TARSKI:def_4; reconsider A = A as Subset of T by A2; consider B being Subset of T such that A3: A = Cl B and A4: B in Int F by A2, PCOMPS_1:def_2; consider D being Subset of T such that A5: B = Int D and A6: D in F by A4, Def1; ex P being set st ( x in P & P in Cl (Int (Cl F)) ) proof take Cl (Int (Cl D)) ; ::_thesis: ( x in Cl (Int (Cl D)) & Cl (Int (Cl D)) in Cl (Int (Cl F)) ) Cl D in Cl F by A6, PCOMPS_1:def_2; then A7: Int (Cl D) in Int (Cl F) by Def1; A c= Cl (Int (Cl D)) by A3, A5, Th2; hence ( x in Cl (Int (Cl D)) & Cl (Int (Cl D)) in Cl (Int (Cl F)) ) by A1, A7, PCOMPS_1:def_2; ::_thesis: verum end; hence x in union (Cl (Int (Cl F))) by TARSKI:def_4; ::_thesis: verum end; hence union (Cl (Int F)) c= union (Cl (Int (Cl F))) by TARSKI:def_3; ::_thesis: verum end; theorem :: TDLAT_2:40 for T being non empty TopSpace for F being Subset-Family of T holds meet (Cl (Int F)) c= meet (Cl (Int (Cl F))) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds meet (Cl (Int F)) c= meet (Cl (Int (Cl F))) let F be Subset-Family of T; ::_thesis: meet (Cl (Int F)) c= meet (Cl (Int (Cl F))) now__::_thesis:_meet_(Cl_(Int_F))_c=_meet_(Cl_(Int_(Cl_F))) percases ( F = {} or F <> {} ) ; suppose F = {} ; ::_thesis: meet (Cl (Int F)) c= meet (Cl (Int (Cl F))) hence meet (Cl (Int F)) c= meet (Cl (Int (Cl F))) by Th9; ::_thesis: verum end; suppose F <> {} ; ::_thesis: meet (Cl (Int F)) c= meet (Cl (Int (Cl F))) then Cl F <> {} by Th9; then Int (Cl F) <> {} by Th19; then A1: Cl (Int (Cl F)) <> {} by Th9; now__::_thesis:_for_x_being_set_st_x_in_meet_(Cl_(Int_F))_holds_ x_in_meet_(Cl_(Int_(Cl_F))) let x be set ; ::_thesis: ( x in meet (Cl (Int F)) implies x in meet (Cl (Int (Cl F))) ) assume A2: x in meet (Cl (Int F)) ; ::_thesis: x in meet (Cl (Int (Cl F))) for A being set st A in Cl (Int (Cl F)) holds x in A proof let A be set ; ::_thesis: ( A in Cl (Int (Cl F)) implies x in A ) assume A3: A in Cl (Int (Cl F)) ; ::_thesis: x in A then reconsider A = A as Subset of T ; consider B being Subset of T such that A4: A = Cl B and A5: B in Int (Cl F) by A3, PCOMPS_1:def_2; consider D being Subset of T such that A6: B = Int D and A7: D in Cl F by A5, Def1; consider E being Subset of T such that A8: D = Cl E and A9: E in F by A7, PCOMPS_1:def_2; Int E in Int F by A9, Def1; then Cl (Int E) in Cl (Int F) by PCOMPS_1:def_2; then A10: x in Cl (Int E) by A2, SETFAM_1:def_1; Cl (Int E) c= Cl (Int (Cl E)) by Th2; hence x in A by A4, A6, A8, A10; ::_thesis: verum end; hence x in meet (Cl (Int (Cl F))) by A1, SETFAM_1:def_1; ::_thesis: verum end; hence meet (Cl (Int F)) c= meet (Cl (Int (Cl F))) by TARSKI:def_3; ::_thesis: verum end; end; end; hence meet (Cl (Int F)) c= meet (Cl (Int (Cl F))) ; ::_thesis: verum end; theorem :: TDLAT_2:41 for T being non empty TopSpace for F being Subset-Family of T holds union (Int (Cl (Int F))) c= union (Int (Cl F)) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Int (Cl (Int F))) c= union (Int (Cl F)) let F be Subset-Family of T; ::_thesis: union (Int (Cl (Int F))) c= union (Int (Cl F)) now__::_thesis:_for_x_being_set_st_x_in_union_(Int_(Cl_(Int_F)))_holds_ x_in_union_(Int_(Cl_F)) let x be set ; ::_thesis: ( x in union (Int (Cl (Int F))) implies x in union (Int (Cl F)) ) assume x in union (Int (Cl (Int F))) ; ::_thesis: x in union (Int (Cl F)) then consider A being set such that A1: x in A and A2: A in Int (Cl (Int F)) by TARSKI:def_4; reconsider A = A as Subset of T by A2; consider B being Subset of T such that A3: A = Int B and A4: B in Cl (Int F) by A2, Def1; consider D being Subset of T such that A5: B = Cl D and A6: D in Int F by A4, PCOMPS_1:def_2; consider E being Subset of T such that A7: D = Int E and A8: E in F by A6, Def1; ex P being set st ( x in P & P in Int (Cl F) ) proof take Int (Cl E) ; ::_thesis: ( x in Int (Cl E) & Int (Cl E) in Int (Cl F) ) A9: Cl E in Cl F by A8, PCOMPS_1:def_2; A c= Int (Cl E) by A3, A5, A7, Th1; hence ( x in Int (Cl E) & Int (Cl E) in Int (Cl F) ) by A1, A9, Def1; ::_thesis: verum end; hence x in union (Int (Cl F)) by TARSKI:def_4; ::_thesis: verum end; hence union (Int (Cl (Int F))) c= union (Int (Cl F)) by TARSKI:def_3; ::_thesis: verum end; theorem :: TDLAT_2:42 for T being non empty TopSpace for F being Subset-Family of T holds meet (Int (Cl (Int F))) c= meet (Int (Cl F)) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds meet (Int (Cl (Int F))) c= meet (Int (Cl F)) let F be Subset-Family of T; ::_thesis: meet (Int (Cl (Int F))) c= meet (Int (Cl F)) now__::_thesis:_meet_(Int_(Cl_(Int_F)))_c=_meet_(Int_(Cl_F)) percases ( F = {} or F <> {} ) ; suppose F = {} ; ::_thesis: meet (Int (Cl (Int F))) c= meet (Int (Cl F)) hence meet (Int (Cl (Int F))) c= meet (Int (Cl F)) by Th19; ::_thesis: verum end; suppose F <> {} ; ::_thesis: meet (Int (Cl (Int F))) c= meet (Int (Cl F)) then Cl F <> {} by Th9; then A1: Int (Cl F) <> {} by Th19; now__::_thesis:_for_x_being_set_st_x_in_meet_(Int_(Cl_(Int_F)))_holds_ x_in_meet_(Int_(Cl_F)) let x be set ; ::_thesis: ( x in meet (Int (Cl (Int F))) implies x in meet (Int (Cl F)) ) assume A2: x in meet (Int (Cl (Int F))) ; ::_thesis: x in meet (Int (Cl F)) for A being set st A in Int (Cl F) holds x in A proof let A be set ; ::_thesis: ( A in Int (Cl F) implies x in A ) assume A3: A in Int (Cl F) ; ::_thesis: x in A then reconsider A = A as Subset of T ; consider E being Subset of T such that A4: A = Int E and A5: E in Cl F by A3, Def1; consider B being Subset of T such that A6: E = Cl B and A7: B in F by A5, PCOMPS_1:def_2; Int B in Int F by A7, Def1; then Cl (Int B) in Cl (Int F) by PCOMPS_1:def_2; then Int (Cl (Int B)) in Int (Cl (Int F)) by Def1; then A8: x in Int (Cl (Int B)) by A2, SETFAM_1:def_1; Int (Cl (Int B)) c= Int (Cl B) by Th1; hence x in A by A4, A6, A8; ::_thesis: verum end; hence x in meet (Int (Cl F)) by A1, SETFAM_1:def_1; ::_thesis: verum end; hence meet (Int (Cl (Int F))) c= meet (Int (Cl F)) by TARSKI:def_3; ::_thesis: verum end; end; end; hence meet (Int (Cl (Int F))) c= meet (Int (Cl F)) ; ::_thesis: verum end; theorem :: TDLAT_2:43 for T being non empty TopSpace for F being Subset-Family of T holds union (Int (Cl (Int F))) c= union (Cl (Int F)) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Int (Cl (Int F))) c= union (Cl (Int F)) let F be Subset-Family of T; ::_thesis: union (Int (Cl (Int F))) c= union (Cl (Int F)) now__::_thesis:_for_x_being_set_st_x_in_union_(Int_(Cl_(Int_F)))_holds_ x_in_union_(Cl_(Int_F)) let x be set ; ::_thesis: ( x in union (Int (Cl (Int F))) implies x in union (Cl (Int F)) ) assume x in union (Int (Cl (Int F))) ; ::_thesis: x in union (Cl (Int F)) then consider A being set such that A1: x in A and A2: A in Int (Cl (Int F)) by TARSKI:def_4; reconsider A = A as Subset of T by A2; consider B being Subset of T such that A3: A = Int B and A4: B in Cl (Int F) by A2, Def1; consider D being Subset of T such that A5: B = Cl D and A6: D in Int F by A4, PCOMPS_1:def_2; consider E being Subset of T such that A7: D = Int E and A8: E in F by A6, Def1; ex P being set st ( x in P & P in Cl (Int F) ) proof take Cl (Int E) ; ::_thesis: ( x in Cl (Int E) & Cl (Int E) in Cl (Int F) ) A9: Int E in Int F by A8, Def1; A c= Cl (Int E) by A3, A5, A7, Th1; hence ( x in Cl (Int E) & Cl (Int E) in Cl (Int F) ) by A1, A9, PCOMPS_1:def_2; ::_thesis: verum end; hence x in union (Cl (Int F)) by TARSKI:def_4; ::_thesis: verum end; hence union (Int (Cl (Int F))) c= union (Cl (Int F)) by TARSKI:def_3; ::_thesis: verum end; theorem :: TDLAT_2:44 for T being non empty TopSpace for F being Subset-Family of T holds meet (Int (Cl (Int F))) c= meet (Cl (Int F)) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds meet (Int (Cl (Int F))) c= meet (Cl (Int F)) let F be Subset-Family of T; ::_thesis: meet (Int (Cl (Int F))) c= meet (Cl (Int F)) now__::_thesis:_meet_(Int_(Cl_(Int_F)))_c=_meet_(Cl_(Int_F)) percases ( F = {} or F <> {} ) ; suppose F = {} ; ::_thesis: meet (Int (Cl (Int F))) c= meet (Cl (Int F)) then Int F = {} by Th19; then Cl (Int F) = {} by Th9; hence meet (Int (Cl (Int F))) c= meet (Cl (Int F)) by Th19; ::_thesis: verum end; suppose F <> {} ; ::_thesis: meet (Int (Cl (Int F))) c= meet (Cl (Int F)) then Int F <> {} by Th19; then A1: Cl (Int F) <> {} by Th9; now__::_thesis:_for_x_being_set_st_x_in_meet_(Int_(Cl_(Int_F)))_holds_ x_in_meet_(Cl_(Int_F)) let x be set ; ::_thesis: ( x in meet (Int (Cl (Int F))) implies x in meet (Cl (Int F)) ) assume A2: x in meet (Int (Cl (Int F))) ; ::_thesis: x in meet (Cl (Int F)) for A being set st A in Cl (Int F) holds x in A proof let A be set ; ::_thesis: ( A in Cl (Int F) implies x in A ) assume A3: A in Cl (Int F) ; ::_thesis: x in A then reconsider A = A as Subset of T ; consider E being Subset of T such that A4: A = Cl E and A5: E in Int F by A3, PCOMPS_1:def_2; consider B being Subset of T such that A6: E = Int B and A7: B in F by A5, Def1; Int B in Int F by A7, Def1; then Cl (Int B) in Cl (Int F) by PCOMPS_1:def_2; then Int (Cl (Int B)) in Int (Cl (Int F)) by Def1; then A8: x in Int (Cl (Int B)) by A2, SETFAM_1:def_1; Int (Cl (Int B)) c= Cl (Int B) by Th1; hence x in A by A4, A6, A8; ::_thesis: verum end; hence x in meet (Cl (Int F)) by A1, SETFAM_1:def_1; ::_thesis: verum end; hence meet (Int (Cl (Int F))) c= meet (Cl (Int F)) by TARSKI:def_3; ::_thesis: verum end; end; end; hence meet (Int (Cl (Int F))) c= meet (Cl (Int F)) ; ::_thesis: verum end; theorem :: TDLAT_2:45 for T being non empty TopSpace for F being Subset-Family of T holds union (Cl (Int (Cl F))) c= union (Cl F) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Cl (Int (Cl F))) c= union (Cl F) let F be Subset-Family of T; ::_thesis: union (Cl (Int (Cl F))) c= union (Cl F) now__::_thesis:_for_x_being_set_st_x_in_union_(Cl_(Int_(Cl_F)))_holds_ x_in_union_(Cl_F) let x be set ; ::_thesis: ( x in union (Cl (Int (Cl F))) implies x in union (Cl F) ) assume x in union (Cl (Int (Cl F))) ; ::_thesis: x in union (Cl F) then consider A being set such that A1: x in A and A2: A in Cl (Int (Cl F)) by TARSKI:def_4; reconsider A = A as Subset of T by A2; consider B being Subset of T such that A3: A = Cl B and A4: B in Int (Cl F) by A2, PCOMPS_1:def_2; consider D being Subset of T such that A5: B = Int D and A6: D in Cl F by A4, Def1; consider E being Subset of T such that A7: D = Cl E and A8: E in F by A6, PCOMPS_1:def_2; ex P being set st ( x in P & P in Cl F ) proof take Cl E ; ::_thesis: ( x in Cl E & Cl E in Cl F ) A c= Cl E by A3, A5, A7, TDLAT_1:3; hence ( x in Cl E & Cl E in Cl F ) by A1, A8, PCOMPS_1:def_2; ::_thesis: verum end; hence x in union (Cl F) by TARSKI:def_4; ::_thesis: verum end; hence union (Cl (Int (Cl F))) c= union (Cl F) by TARSKI:def_3; ::_thesis: verum end; theorem :: TDLAT_2:46 for T being non empty TopSpace for F being Subset-Family of T holds meet (Cl (Int (Cl F))) c= meet (Cl F) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds meet (Cl (Int (Cl F))) c= meet (Cl F) let F be Subset-Family of T; ::_thesis: meet (Cl (Int (Cl F))) c= meet (Cl F) now__::_thesis:_meet_(Cl_(Int_(Cl_F)))_c=_meet_(Cl_F) percases ( F = {} or F <> {} ) ; supposeA1: F = {} ; ::_thesis: meet (Cl (Int (Cl F))) c= meet (Cl F) then Cl F = {} by Th9; hence meet (Cl (Int (Cl F))) c= meet (Cl F) by A1, Th19; ::_thesis: verum end; suppose F <> {} ; ::_thesis: meet (Cl (Int (Cl F))) c= meet (Cl F) then A2: Cl F <> {} by Th9; now__::_thesis:_for_x_being_set_st_x_in_meet_(Cl_(Int_(Cl_F)))_holds_ x_in_meet_(Cl_F) let x be set ; ::_thesis: ( x in meet (Cl (Int (Cl F))) implies x in meet (Cl F) ) assume A3: x in meet (Cl (Int (Cl F))) ; ::_thesis: x in meet (Cl F) for A being set st A in Cl F holds x in A proof let A be set ; ::_thesis: ( A in Cl F implies x in A ) assume A4: A in Cl F ; ::_thesis: x in A then reconsider A = A as Subset of T ; consider B being Subset of T such that A5: A = Cl B and A6: B in F by A4, PCOMPS_1:def_2; Cl B in Cl F by A6, PCOMPS_1:def_2; then Int (Cl B) in Int (Cl F) by Def1; then Cl (Int (Cl B)) in Cl (Int (Cl F)) by PCOMPS_1:def_2; then A7: x in Cl (Int (Cl B)) by A3, SETFAM_1:def_1; Cl (Int (Cl B)) c= Cl B by TDLAT_1:3; hence x in A by A5, A7; ::_thesis: verum end; hence x in meet (Cl F) by A2, SETFAM_1:def_1; ::_thesis: verum end; hence meet (Cl (Int (Cl F))) c= meet (Cl F) by TARSKI:def_3; ::_thesis: verum end; end; end; hence meet (Cl (Int (Cl F))) c= meet (Cl F) ; ::_thesis: verum end; theorem :: TDLAT_2:47 for T being non empty TopSpace for F being Subset-Family of T holds union (Int F) c= union (Int (Cl (Int F))) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Int F) c= union (Int (Cl (Int F))) let F be Subset-Family of T; ::_thesis: union (Int F) c= union (Int (Cl (Int F))) now__::_thesis:_for_x_being_set_st_x_in_union_(Int_F)_holds_ x_in_union_(Int_(Cl_(Int_F))) let x be set ; ::_thesis: ( x in union (Int F) implies x in union (Int (Cl (Int F))) ) assume x in union (Int F) ; ::_thesis: x in union (Int (Cl (Int F))) then consider A being set such that A1: x in A and A2: A in Int F by TARSKI:def_4; reconsider A = A as Subset of T by A2; consider B being Subset of T such that A3: A = Int B and A4: B in F by A2, Def1; ex P being set st ( x in P & P in Int (Cl (Int F)) ) proof take Int (Cl (Int B)) ; ::_thesis: ( x in Int (Cl (Int B)) & Int (Cl (Int B)) in Int (Cl (Int F)) ) Int B in Int F by A4, Def1; then A5: Cl (Int B) in Cl (Int F) by PCOMPS_1:def_2; A c= Int (Cl (Int B)) by A3, TDLAT_1:4; hence ( x in Int (Cl (Int B)) & Int (Cl (Int B)) in Int (Cl (Int F)) ) by A1, A5, Def1; ::_thesis: verum end; hence x in union (Int (Cl (Int F))) by TARSKI:def_4; ::_thesis: verum end; hence union (Int F) c= union (Int (Cl (Int F))) by TARSKI:def_3; ::_thesis: verum end; theorem :: TDLAT_2:48 for T being non empty TopSpace for F being Subset-Family of T holds meet (Int F) c= meet (Int (Cl (Int F))) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds meet (Int F) c= meet (Int (Cl (Int F))) let F be Subset-Family of T; ::_thesis: meet (Int F) c= meet (Int (Cl (Int F))) now__::_thesis:_meet_(Int_F)_c=_meet_(Int_(Cl_(Int_F))) percases ( F = {} or F <> {} ) ; supposeA1: F = {} ; ::_thesis: meet (Int F) c= meet (Int (Cl (Int F))) then Int F = {} by Th19; hence meet (Int F) c= meet (Int (Cl (Int F))) by A1, Th9; ::_thesis: verum end; suppose F <> {} ; ::_thesis: meet (Int F) c= meet (Int (Cl (Int F))) then Int F <> {} by Th19; then Cl (Int F) <> {} by Th9; then A2: Int (Cl (Int F)) <> {} by Th19; now__::_thesis:_for_x_being_set_st_x_in_meet_(Int_F)_holds_ x_in_meet_(Int_(Cl_(Int_F))) let x be set ; ::_thesis: ( x in meet (Int F) implies x in meet (Int (Cl (Int F))) ) assume A3: x in meet (Int F) ; ::_thesis: x in meet (Int (Cl (Int F))) for A being set st A in Int (Cl (Int F)) holds x in A proof let A be set ; ::_thesis: ( A in Int (Cl (Int F)) implies x in A ) assume A4: A in Int (Cl (Int F)) ; ::_thesis: x in A then reconsider A = A as Subset of T ; consider E being Subset of T such that A5: A = Int E and A6: E in Cl (Int F) by A4, Def1; consider B being Subset of T such that A7: E = Cl B and A8: B in Int F by A6, PCOMPS_1:def_2; consider D being Subset of T such that A9: B = Int D and A10: D in F by A8, Def1; Int D in Int F by A10, Def1; then A11: x in Int D by A3, SETFAM_1:def_1; Int D c= Int (Cl (Int D)) by TDLAT_1:4; hence x in A by A5, A7, A9, A11; ::_thesis: verum end; hence x in meet (Int (Cl (Int F))) by A2, SETFAM_1:def_1; ::_thesis: verum end; hence meet (Int F) c= meet (Int (Cl (Int F))) by TARSKI:def_3; ::_thesis: verum end; end; end; hence meet (Int F) c= meet (Int (Cl (Int F))) ; ::_thesis: verum end; theorem Th49: :: TDLAT_2:49 for T being non empty TopSpace for F being Subset-Family of T holds union (Cl (Int F)) c= Cl (Int (union F)) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Cl (Int F)) c= Cl (Int (union F)) let F be Subset-Family of T; ::_thesis: union (Cl (Int F)) c= Cl (Int (union F)) A1: Cl (union (Int F)) c= Cl (Int (union F)) by Th28, PRE_TOPC:19; union (Cl (Int F)) c= Cl (union (Int F)) by Th15; hence union (Cl (Int F)) c= Cl (Int (union F)) by A1, XBOOLE_1:1; ::_thesis: verum end; theorem Th50: :: TDLAT_2:50 for T being non empty TopSpace for F being Subset-Family of T holds Cl (Int (meet F)) c= meet (Cl (Int F)) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Cl (Int (meet F)) c= meet (Cl (Int F)) let F be Subset-Family of T; ::_thesis: Cl (Int (meet F)) c= meet (Cl (Int F)) A1: Cl (meet (Int F)) c= meet (Cl (Int F)) by Th14; Cl (Int (meet F)) c= Cl (meet (Int F)) by Th29, PRE_TOPC:19; hence Cl (Int (meet F)) c= meet (Cl (Int F)) by A1, XBOOLE_1:1; ::_thesis: verum end; theorem Th51: :: TDLAT_2:51 for T being non empty TopSpace for F being Subset-Family of T holds union (Int (Cl F)) c= Int (Cl (union F)) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Int (Cl F)) c= Int (Cl (union F)) let F be Subset-Family of T; ::_thesis: union (Int (Cl F)) c= Int (Cl (union F)) A1: Int (union (Cl F)) c= Int (Cl (union F)) by Th15, TOPS_1:19; union (Int (Cl F)) c= Int (union (Cl F)) by Th28; hence union (Int (Cl F)) c= Int (Cl (union F)) by A1, XBOOLE_1:1; ::_thesis: verum end; theorem Th52: :: TDLAT_2:52 for T being non empty TopSpace for F being Subset-Family of T holds Int (Cl (meet F)) c= meet (Int (Cl F)) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Int (Cl (meet F)) c= meet (Int (Cl F)) let F be Subset-Family of T; ::_thesis: Int (Cl (meet F)) c= meet (Int (Cl F)) A1: Int (meet (Cl F)) c= meet (Int (Cl F)) by Th29; Int (Cl (meet F)) c= Int (meet (Cl F)) by Th14, TOPS_1:19; hence Int (Cl (meet F)) c= meet (Int (Cl F)) by A1, XBOOLE_1:1; ::_thesis: verum end; theorem :: TDLAT_2:53 for T being non empty TopSpace for F being Subset-Family of T holds union (Cl (Int (Cl F))) c= Cl (Int (Cl (union F))) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Cl (Int (Cl F))) c= Cl (Int (Cl (union F))) let F be Subset-Family of T; ::_thesis: union (Cl (Int (Cl F))) c= Cl (Int (Cl (union F))) A1: Cl (union (Int (Cl F))) c= Cl (Int (Cl (union F))) by Th51, PRE_TOPC:19; union (Cl (Int (Cl F))) c= Cl (union (Int (Cl F))) by Th15; hence union (Cl (Int (Cl F))) c= Cl (Int (Cl (union F))) by A1, XBOOLE_1:1; ::_thesis: verum end; theorem :: TDLAT_2:54 for T being non empty TopSpace for F being Subset-Family of T holds Cl (Int (Cl (meet F))) c= meet (Cl (Int (Cl F))) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Cl (Int (Cl (meet F))) c= meet (Cl (Int (Cl F))) let F be Subset-Family of T; ::_thesis: Cl (Int (Cl (meet F))) c= meet (Cl (Int (Cl F))) A1: Cl (Int (Cl (meet F))) c= Cl (meet (Int (Cl F))) by Th52, PRE_TOPC:19; Cl (meet (Int (Cl F))) c= meet (Cl (Int (Cl F))) by Th14; hence Cl (Int (Cl (meet F))) c= meet (Cl (Int (Cl F))) by A1, XBOOLE_1:1; ::_thesis: verum end; theorem :: TDLAT_2:55 for T being non empty TopSpace for F being Subset-Family of T holds union (Int (Cl (Int F))) c= Int (Cl (Int (union F))) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds union (Int (Cl (Int F))) c= Int (Cl (Int (union F))) let F be Subset-Family of T; ::_thesis: union (Int (Cl (Int F))) c= Int (Cl (Int (union F))) A1: Int (union (Cl (Int F))) c= Int (Cl (Int (union F))) by Th49, TOPS_1:19; union (Int (Cl (Int F))) c= Int (union (Cl (Int F))) by Th28; hence union (Int (Cl (Int F))) c= Int (Cl (Int (union F))) by A1, XBOOLE_1:1; ::_thesis: verum end; theorem :: TDLAT_2:56 for T being non empty TopSpace for F being Subset-Family of T holds Int (Cl (Int (meet F))) c= meet (Int (Cl (Int F))) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds Int (Cl (Int (meet F))) c= meet (Int (Cl (Int F))) let F be Subset-Family of T; ::_thesis: Int (Cl (Int (meet F))) c= meet (Int (Cl (Int F))) A1: Int (Cl (Int (meet F))) c= Int (meet (Cl (Int F))) by Th50, TOPS_1:19; Int (meet (Cl (Int F))) c= meet (Int (Cl (Int F))) by Th29; hence Int (Cl (Int (meet F))) c= meet (Int (Cl (Int F))) by A1, XBOOLE_1:1; ::_thesis: verum end; theorem Th57: :: TDLAT_2:57 for T being non empty TopSpace for F being Subset-Family of T st ( for A being Subset of T st A in F holds A c= Cl (Int A) ) holds ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st ( for A being Subset of T st A in F holds A c= Cl (Int A) ) holds ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) ) let F be Subset-Family of T; ::_thesis: ( ( for A being Subset of T st A in F holds A c= Cl (Int A) ) implies ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) ) ) A1: Cl (Int (Cl (union F))) c= Cl (Cl (union F)) by PRE_TOPC:19, TOPS_1:16; assume A2: for A being Subset of T st A in F holds A c= Cl (Int A) ; ::_thesis: ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) ) A3: now__::_thesis:_for_A0_being_set_st_A0_in_F_holds_ A0_c=_Cl_(Int_(union_F)) let A0 be set ; ::_thesis: ( A0 in F implies A0 c= Cl (Int (union F)) ) assume A4: A0 in F ; ::_thesis: A0 c= Cl (Int (union F)) then reconsider A = A0 as Subset of T ; Int A c= Int (union F) by A4, TOPS_1:19, ZFMISC_1:74; then A5: Cl (Int A) c= Cl (Int (union F)) by PRE_TOPC:19; A c= Cl (Int A) by A2, A4; hence A0 c= Cl (Int (union F)) by A5, XBOOLE_1:1; ::_thesis: verum end; hence union F c= Cl (Int (union F)) by ZFMISC_1:76; ::_thesis: Cl (union F) = Cl (Int (Cl (union F))) Int (union F) c= Int (Cl (union F)) by PRE_TOPC:18, TOPS_1:19; then A6: Cl (Int (union F)) c= Cl (Int (Cl (union F))) by PRE_TOPC:19; union F c= Cl (Int (union F)) by A3, ZFMISC_1:76; then Cl (union F) c= Cl (Cl (Int (union F))) by PRE_TOPC:19; then Cl (union F) c= Cl (Int (Cl (union F))) by A6, XBOOLE_1:1; hence Cl (union F) = Cl (Int (Cl (union F))) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th58: :: TDLAT_2:58 for T being non empty TopSpace for F being Subset-Family of T st ( for A being Subset of T st A in F holds Int (Cl A) c= A ) holds ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st ( for A being Subset of T st A in F holds Int (Cl A) c= A ) holds ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) ) let F be Subset-Family of T; ::_thesis: ( ( for A being Subset of T st A in F holds Int (Cl A) c= A ) implies ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) ) ) A1: Int (Int (meet F)) c= Int (Cl (Int (meet F))) by PRE_TOPC:18, TOPS_1:19; assume A2: for A being Subset of T st A in F holds Int (Cl A) c= A ; ::_thesis: ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) ) thus Int (Cl (meet F)) c= meet F ::_thesis: Int (Cl (Int (meet F))) = Int (meet F) proof now__::_thesis:_Int_(Cl_(meet_F))_c=_meet_F percases ( F = {} or F <> {} ) ; supposeA3: F = {} ; ::_thesis: Int (Cl (meet F)) c= meet F Cl ({} T) = {} T by PRE_TOPC:22; hence Int (Cl (meet F)) c= meet F by A3, SETFAM_1:1; ::_thesis: verum end; supposeA4: F <> {} ; ::_thesis: Int (Cl (meet F)) c= meet F now__::_thesis:_for_A0_being_set_st_A0_in_F_holds_ Int_(Cl_(meet_F))_c=_A0 let A0 be set ; ::_thesis: ( A0 in F implies Int (Cl (meet F)) c= A0 ) assume A5: A0 in F ; ::_thesis: Int (Cl (meet F)) c= A0 then reconsider A = A0 as Subset of T ; Cl (meet F) c= Cl A by A5, PRE_TOPC:19, SETFAM_1:3; then A6: Int (Cl (meet F)) c= Int (Cl A) by TOPS_1:19; Int (Cl A) c= A by A2, A5; hence Int (Cl (meet F)) c= A0 by A6, XBOOLE_1:1; ::_thesis: verum end; hence Int (Cl (meet F)) c= meet F by A4, SETFAM_1:5; ::_thesis: verum end; end; end; hence Int (Cl (meet F)) c= meet F ; ::_thesis: verum end; then A7: Int (Int (Cl (meet F))) c= Int (meet F) by TOPS_1:19; Cl (Int (meet F)) c= Cl (meet F) by PRE_TOPC:19, TOPS_1:16; then Int (Cl (Int (meet F))) c= Int (Cl (meet F)) by TOPS_1:19; then Int (Cl (Int (meet F))) c= Int (meet F) by A7, XBOOLE_1:1; hence Int (Cl (Int (meet F))) = Int (meet F) by A1, XBOOLE_0:def_10; ::_thesis: verum end; begin theorem Th59: :: TDLAT_2:59 for T being non empty TopSpace for A, B being Subset of T st B is condensed holds ( (Int (Cl (A \/ B))) \/ (A \/ B) = B iff A c= B ) proof let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st B is condensed holds ( (Int (Cl (A \/ B))) \/ (A \/ B) = B iff A c= B ) let A, B be Subset of T; ::_thesis: ( B is condensed implies ( (Int (Cl (A \/ B))) \/ (A \/ B) = B iff A c= B ) ) assume A1: B is condensed ; ::_thesis: ( (Int (Cl (A \/ B))) \/ (A \/ B) = B iff A c= B ) thus ( (Int (Cl (A \/ B))) \/ (A \/ B) = B implies A c= B ) ::_thesis: ( A c= B implies (Int (Cl (A \/ B))) \/ (A \/ B) = B ) proof assume (Int (Cl (A \/ B))) \/ (A \/ B) = B ; ::_thesis: A c= B then A2: A \/ B c= B by XBOOLE_1:7; A c= A \/ B by XBOOLE_1:7; hence A c= B by A2, XBOOLE_1:1; ::_thesis: verum end; thus ( A c= B implies (Int (Cl (A \/ B))) \/ (A \/ B) = B ) ::_thesis: verum proof assume A c= B ; ::_thesis: (Int (Cl (A \/ B))) \/ (A \/ B) = B then A3: A \/ B = B by XBOOLE_1:12; then Int (Cl (A \/ B)) c= B by A1, TOPS_1:def_6; hence (Int (Cl (A \/ B))) \/ (A \/ B) = B by A3, XBOOLE_1:12; ::_thesis: verum end; end; theorem :: TDLAT_2:60 for T being non empty TopSpace for A, B being Subset of T st A is condensed holds ( (Cl (Int (A /\ B))) /\ (A /\ B) = A iff A c= B ) proof let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A is condensed holds ( (Cl (Int (A /\ B))) /\ (A /\ B) = A iff A c= B ) let A, B be Subset of T; ::_thesis: ( A is condensed implies ( (Cl (Int (A /\ B))) /\ (A /\ B) = A iff A c= B ) ) assume A1: A is condensed ; ::_thesis: ( (Cl (Int (A /\ B))) /\ (A /\ B) = A iff A c= B ) thus ( (Cl (Int (A /\ B))) /\ (A /\ B) = A implies A c= B ) ::_thesis: ( A c= B implies (Cl (Int (A /\ B))) /\ (A /\ B) = A ) proof assume (Cl (Int (A /\ B))) /\ (A /\ B) = A ; ::_thesis: A c= B then A2: A c= A /\ B by XBOOLE_1:17; A /\ B c= B by XBOOLE_1:17; hence A c= B by A2, XBOOLE_1:1; ::_thesis: verum end; thus ( A c= B implies (Cl (Int (A /\ B))) /\ (A /\ B) = A ) ::_thesis: verum proof assume A c= B ; ::_thesis: (Cl (Int (A /\ B))) /\ (A /\ B) = A then A3: A /\ B = A by XBOOLE_1:28; then A c= Cl (Int (A /\ B)) by A1, TOPS_1:def_6; hence (Cl (Int (A /\ B))) /\ (A /\ B) = A by A3, XBOOLE_1:28; ::_thesis: verum end; end; theorem :: TDLAT_2:61 for T being non empty TopSpace for A, B being Subset of T st A is closed_condensed & B is closed_condensed holds ( Int A c= Int B iff A c= B ) proof let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A is closed_condensed & B is closed_condensed holds ( Int A c= Int B iff A c= B ) let A, B be Subset of T; ::_thesis: ( A is closed_condensed & B is closed_condensed implies ( Int A c= Int B iff A c= B ) ) assume that A1: A is closed_condensed and A2: B is closed_condensed ; ::_thesis: ( Int A c= Int B iff A c= B ) thus ( Int A c= Int B implies A c= B ) ::_thesis: ( A c= B implies Int A c= Int B ) proof assume Int A c= Int B ; ::_thesis: A c= B then A3: Cl (Int A) c= Cl (Int B) by PRE_TOPC:19; Cl (Int A) = A by A1, TOPS_1:def_7; hence A c= B by A2, A3, TOPS_1:def_7; ::_thesis: verum end; thus ( A c= B implies Int A c= Int B ) by TOPS_1:19; ::_thesis: verum end; theorem :: TDLAT_2:62 for T being non empty TopSpace for A, B being Subset of T st A is open_condensed & B is open_condensed holds ( Cl A c= Cl B iff A c= B ) proof let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A is open_condensed & B is open_condensed holds ( Cl A c= Cl B iff A c= B ) let A, B be Subset of T; ::_thesis: ( A is open_condensed & B is open_condensed implies ( Cl A c= Cl B iff A c= B ) ) assume that A1: A is open_condensed and A2: B is open_condensed ; ::_thesis: ( Cl A c= Cl B iff A c= B ) thus ( Cl A c= Cl B implies A c= B ) ::_thesis: ( A c= B implies Cl A c= Cl B ) proof assume Cl A c= Cl B ; ::_thesis: A c= B then A3: Int (Cl A) c= Int (Cl B) by TOPS_1:19; Int (Cl A) = A by A1, TOPS_1:def_8; hence A c= B by A2, A3, TOPS_1:def_8; ::_thesis: verum end; thus ( A c= B implies Cl A c= Cl B ) by PRE_TOPC:19; ::_thesis: verum end; theorem :: TDLAT_2:63 for T being non empty TopSpace for A, B being Subset of T st A is closed_condensed & A c= B holds Cl (Int (A /\ B)) = A proof let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A is closed_condensed & A c= B holds Cl (Int (A /\ B)) = A let A, B be Subset of T; ::_thesis: ( A is closed_condensed & A c= B implies Cl (Int (A /\ B)) = A ) assume A1: A is closed_condensed ; ::_thesis: ( not A c= B or Cl (Int (A /\ B)) = A ) assume A c= B ; ::_thesis: Cl (Int (A /\ B)) = A then A /\ B = A by XBOOLE_1:28; hence Cl (Int (A /\ B)) = A by A1, TOPS_1:def_7; ::_thesis: verum end; theorem Th64: :: TDLAT_2:64 for T being non empty TopSpace for A, B being Subset of T st B is open_condensed & A c= B holds Int (Cl (A \/ B)) = B proof let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st B is open_condensed & A c= B holds Int (Cl (A \/ B)) = B let A, B be Subset of T; ::_thesis: ( B is open_condensed & A c= B implies Int (Cl (A \/ B)) = B ) assume A1: B is open_condensed ; ::_thesis: ( not A c= B or Int (Cl (A \/ B)) = B ) assume A c= B ; ::_thesis: Int (Cl (A \/ B)) = B then A \/ B = B by XBOOLE_1:12; hence Int (Cl (A \/ B)) = B by A1, TOPS_1:def_8; ::_thesis: verum end; definition let T be non empty TopSpace; let IT be Subset-Family of T; attrIT is domains-family means :Def2: :: TDLAT_2:def 2 for A being Subset of T st A in IT holds A is condensed ; end; :: deftheorem Def2 defines domains-family TDLAT_2:def_2_:_ for T being non empty TopSpace for IT being Subset-Family of T holds ( IT is domains-family iff for A being Subset of T st A in IT holds A is condensed ); theorem Th65: :: TDLAT_2:65 for T being non empty TopSpace for F being Subset-Family of T holds ( F c= Domains_of T iff F is domains-family ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds ( F c= Domains_of T iff F is domains-family ) let F be Subset-Family of T; ::_thesis: ( F c= Domains_of T iff F is domains-family ) thus ( F c= Domains_of T implies F is domains-family ) ::_thesis: ( F is domains-family implies F c= Domains_of T ) proof assume A1: F c= Domains_of T ; ::_thesis: F is domains-family now__::_thesis:_for_A_being_Subset_of_T_st_A_in_F_holds_ A_is_condensed let A be Subset of T; ::_thesis: ( A in F implies A is condensed ) assume A in F ; ::_thesis: A is condensed then A in Domains_of T by A1; then A in { P where P is Subset of T : P is condensed } by TDLAT_1:def_1; then ex Q being Subset of T st ( Q = A & Q is condensed ) ; hence A is condensed ; ::_thesis: verum end; hence F is domains-family by Def2; ::_thesis: verum end; thus ( F is domains-family implies F c= Domains_of T ) ::_thesis: verum proof assume A2: F is domains-family ; ::_thesis: F c= Domains_of T for X being set st X in F holds X in Domains_of T proof let X be set ; ::_thesis: ( X in F implies X in Domains_of T ) assume A3: X in F ; ::_thesis: X in Domains_of T then reconsider X0 = X as Subset of T ; X0 is condensed by A2, A3, Def2; then X0 in { P where P is Subset of T : P is condensed } ; hence X in Domains_of T by TDLAT_1:def_1; ::_thesis: verum end; hence F c= Domains_of T by TARSKI:def_3; ::_thesis: verum end; end; theorem Th66: :: TDLAT_2:66 for T being non empty TopSpace for F being Subset-Family of T st F is domains-family holds ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is domains-family holds ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) ) let F be Subset-Family of T; ::_thesis: ( F is domains-family implies ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) ) ) assume A1: F is domains-family ; ::_thesis: ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) ) now__::_thesis:_for_A_being_Subset_of_T_st_A_in_F_holds_ A_c=_Cl_(Int_A) let A be Subset of T; ::_thesis: ( A in F implies A c= Cl (Int A) ) reconsider B = A as Subset of T ; assume A in F ; ::_thesis: A c= Cl (Int A) then B is condensed by A1, Def2; hence A c= Cl (Int A) by TOPS_1:def_6; ::_thesis: verum end; hence ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) ) by Th57; ::_thesis: verum end; theorem Th67: :: TDLAT_2:67 for T being non empty TopSpace for F being Subset-Family of T st F is domains-family holds ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is domains-family holds ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) ) let F be Subset-Family of T; ::_thesis: ( F is domains-family implies ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) ) ) assume A1: F is domains-family ; ::_thesis: ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) ) now__::_thesis:_for_A_being_Subset_of_T_st_A_in_F_holds_ Int_(Cl_A)_c=_A let A be Subset of T; ::_thesis: ( A in F implies Int (Cl A) c= A ) reconsider B = A as Subset of T ; assume A in F ; ::_thesis: Int (Cl A) c= A then B is condensed by A1, Def2; hence Int (Cl A) c= A by TOPS_1:def_6; ::_thesis: verum end; hence ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) ) by Th58; ::_thesis: verum end; theorem Th68: :: TDLAT_2:68 for T being non empty TopSpace for F being Subset-Family of T st F is domains-family holds (union F) \/ (Int (Cl (union F))) is condensed proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is domains-family holds (union F) \/ (Int (Cl (union F))) is condensed let F be Subset-Family of T; ::_thesis: ( F is domains-family implies (union F) \/ (Int (Cl (union F))) is condensed ) A1: Cl (Int (Cl (union F))) c= Cl (Cl (union F)) by PRE_TOPC:19, TOPS_1:16; assume F is domains-family ; ::_thesis: (union F) \/ (Int (Cl (union F))) is condensed then union F c= Cl (Int (union F)) by Th66; then A2: (union F) \/ (Int (Cl (union F))) c= Cl (Int ((union F) \/ (Int (Cl (union F))))) by Th5; Int (Cl ((union F) \/ (Int (Cl (union F))))) = Int ((Cl (union F)) \/ (Cl (Int (Cl (union F))))) by PRE_TOPC:20 .= Int (Cl (union F)) by A1, XBOOLE_1:12 ; then Int (Cl ((union F) \/ (Int (Cl (union F))))) c= (union F) \/ (Int (Cl (union F))) by XBOOLE_1:7; hence (union F) \/ (Int (Cl (union F))) is condensed by A2, TOPS_1:def_6; ::_thesis: verum end; theorem Th69: :: TDLAT_2:69 for T being non empty TopSpace for F being Subset-Family of T holds ( ( for B being Subset of T st B in F holds B c= (union F) \/ (Int (Cl (union F))) ) & ( for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds B c= A ) holds (union F) \/ (Int (Cl (union F))) c= A ) ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds ( ( for B being Subset of T st B in F holds B c= (union F) \/ (Int (Cl (union F))) ) & ( for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds B c= A ) holds (union F) \/ (Int (Cl (union F))) c= A ) ) let F be Subset-Family of T; ::_thesis: ( ( for B being Subset of T st B in F holds B c= (union F) \/ (Int (Cl (union F))) ) & ( for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds B c= A ) holds (union F) \/ (Int (Cl (union F))) c= A ) ) thus for B being Subset of T st B in F holds B c= (union F) \/ (Int (Cl (union F))) ::_thesis: for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds B c= A ) holds (union F) \/ (Int (Cl (union F))) c= A proof let B be Subset of T; ::_thesis: ( B in F implies B c= (union F) \/ (Int (Cl (union F))) ) assume B in F ; ::_thesis: B c= (union F) \/ (Int (Cl (union F))) then A1: B c= union F by ZFMISC_1:74; union F c= (union F) \/ (Int (Cl (union F))) by XBOOLE_1:7; hence B c= (union F) \/ (Int (Cl (union F))) by A1, XBOOLE_1:1; ::_thesis: verum end; thus for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds B c= A ) holds (union F) \/ (Int (Cl (union F))) c= A ::_thesis: verum proof let A be Subset of T; ::_thesis: ( A is condensed & ( for B being Subset of T st B in F holds B c= A ) implies (union F) \/ (Int (Cl (union F))) c= A ) assume A is condensed ; ::_thesis: ( ex B being Subset of T st ( B in F & not B c= A ) or (union F) \/ (Int (Cl (union F))) c= A ) then A2: Int (Cl A) c= A by TOPS_1:def_6; assume for B being Subset of T st B in F holds B c= A ; ::_thesis: (union F) \/ (Int (Cl (union F))) c= A then for P being set st P in F holds P c= A ; then A3: union F c= A by ZFMISC_1:76; then Cl (union F) c= Cl A by PRE_TOPC:19; then Int (Cl (union F)) c= Int (Cl A) by TOPS_1:19; then Int (Cl (union F)) c= A by A2, XBOOLE_1:1; hence (union F) \/ (Int (Cl (union F))) c= A by A3, XBOOLE_1:8; ::_thesis: verum end; end; theorem Th70: :: TDLAT_2:70 for T being non empty TopSpace for F being Subset-Family of T st F is domains-family holds (meet F) /\ (Cl (Int (meet F))) is condensed proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is domains-family holds (meet F) /\ (Cl (Int (meet F))) is condensed let F be Subset-Family of T; ::_thesis: ( F is domains-family implies (meet F) /\ (Cl (Int (meet F))) is condensed ) A1: Int (Int (meet F)) c= Int (Cl (Int (meet F))) by PRE_TOPC:18, TOPS_1:19; assume F is domains-family ; ::_thesis: (meet F) /\ (Cl (Int (meet F))) is condensed then Int (Cl (meet F)) c= meet F by Th67; then A2: Int (Cl ((meet F) /\ (Cl (Int (meet F))))) c= (meet F) /\ (Cl (Int (meet F))) by Th6; Cl (Int ((meet F) /\ (Cl (Int (meet F))))) = Cl ((Int (meet F)) /\ (Int (Cl (Int (meet F))))) by TOPS_1:17 .= Cl (Int (meet F)) by A1, XBOOLE_1:28 ; then (meet F) /\ (Cl (Int (meet F))) c= Cl (Int ((meet F) /\ (Cl (Int (meet F))))) by XBOOLE_1:17; hence (meet F) /\ (Cl (Int (meet F))) is condensed by A2, TOPS_1:def_6; ::_thesis: verum end; theorem Th71: :: TDLAT_2:71 for T being non empty TopSpace for F being Subset-Family of T holds ( ( for B being Subset of T st B in F holds (meet F) /\ (Cl (Int (meet F))) c= B ) & ( F = {} or for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= (meet F) /\ (Cl (Int (meet F))) ) ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds ( ( for B being Subset of T st B in F holds (meet F) /\ (Cl (Int (meet F))) c= B ) & ( F = {} or for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= (meet F) /\ (Cl (Int (meet F))) ) ) let F be Subset-Family of T; ::_thesis: ( ( for B being Subset of T st B in F holds (meet F) /\ (Cl (Int (meet F))) c= B ) & ( F = {} or for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= (meet F) /\ (Cl (Int (meet F))) ) ) thus for B being Subset of T st B in F holds (meet F) /\ (Cl (Int (meet F))) c= B ::_thesis: ( F = {} or for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= (meet F) /\ (Cl (Int (meet F))) ) proof let B be Subset of T; ::_thesis: ( B in F implies (meet F) /\ (Cl (Int (meet F))) c= B ) assume B in F ; ::_thesis: (meet F) /\ (Cl (Int (meet F))) c= B then A1: meet F c= B by SETFAM_1:3; (meet F) /\ (Cl (Int (meet F))) c= meet F by XBOOLE_1:17; hence (meet F) /\ (Cl (Int (meet F))) c= B by A1, XBOOLE_1:1; ::_thesis: verum end; thus ( F = {} or for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= (meet F) /\ (Cl (Int (meet F))) ) ::_thesis: verum proof assume A2: F <> {} ; ::_thesis: for A being Subset of T st A is condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= (meet F) /\ (Cl (Int (meet F))) let A be Subset of T; ::_thesis: ( A is condensed & ( for B being Subset of T st B in F holds A c= B ) implies A c= (meet F) /\ (Cl (Int (meet F))) ) assume A is condensed ; ::_thesis: ( ex B being Subset of T st ( B in F & not A c= B ) or A c= (meet F) /\ (Cl (Int (meet F))) ) then A3: A c= Cl (Int A) by TOPS_1:def_6; assume for B being Subset of T st B in F holds A c= B ; ::_thesis: A c= (meet F) /\ (Cl (Int (meet F))) then for P being set st P in F holds A c= P ; then A4: A c= meet F by A2, SETFAM_1:5; then Int A c= Int (meet F) by TOPS_1:19; then Cl (Int A) c= Cl (Int (meet F)) by PRE_TOPC:19; then A c= Cl (Int (meet F)) by A3, XBOOLE_1:1; hence A c= (meet F) /\ (Cl (Int (meet F))) by A4, XBOOLE_1:19; ::_thesis: verum end; end; definition let T be non empty TopSpace; let IT be Subset-Family of T; attrIT is closed-domains-family means :Def3: :: TDLAT_2:def 3 for A being Subset of T st A in IT holds A is closed_condensed ; end; :: deftheorem Def3 defines closed-domains-family TDLAT_2:def_3_:_ for T being non empty TopSpace for IT being Subset-Family of T holds ( IT is closed-domains-family iff for A being Subset of T st A in IT holds A is closed_condensed ); theorem Th72: :: TDLAT_2:72 for T being non empty TopSpace for F being Subset-Family of T holds ( F c= Closed_Domains_of T iff F is closed-domains-family ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds ( F c= Closed_Domains_of T iff F is closed-domains-family ) let F be Subset-Family of T; ::_thesis: ( F c= Closed_Domains_of T iff F is closed-domains-family ) thus ( F c= Closed_Domains_of T implies F is closed-domains-family ) ::_thesis: ( F is closed-domains-family implies F c= Closed_Domains_of T ) proof assume A1: F c= Closed_Domains_of T ; ::_thesis: F is closed-domains-family now__::_thesis:_for_A_being_Subset_of_T_st_A_in_F_holds_ A_is_closed_condensed let A be Subset of T; ::_thesis: ( A in F implies A is closed_condensed ) assume A in F ; ::_thesis: A is closed_condensed then A in Closed_Domains_of T by A1; then A in { P where P is Subset of T : P is closed_condensed } by TDLAT_1:def_5; then ex Q being Subset of T st ( Q = A & Q is closed_condensed ) ; hence A is closed_condensed ; ::_thesis: verum end; hence F is closed-domains-family by Def3; ::_thesis: verum end; thus ( F is closed-domains-family implies F c= Closed_Domains_of T ) ::_thesis: verum proof assume A2: F is closed-domains-family ; ::_thesis: F c= Closed_Domains_of T for X being set st X in F holds X in Closed_Domains_of T proof let X be set ; ::_thesis: ( X in F implies X in Closed_Domains_of T ) assume A3: X in F ; ::_thesis: X in Closed_Domains_of T then reconsider X0 = X as Subset of T ; X0 is closed_condensed by A2, A3, Def3; then X0 in { P where P is Subset of T : P is closed_condensed } ; hence X in Closed_Domains_of T by TDLAT_1:def_5; ::_thesis: verum end; hence F c= Closed_Domains_of T by TARSKI:def_3; ::_thesis: verum end; end; theorem Th73: :: TDLAT_2:73 for T being non empty TopSpace for F being Subset-Family of T st F is closed-domains-family holds F is domains-family proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is closed-domains-family holds F is domains-family let F be Subset-Family of T; ::_thesis: ( F is closed-domains-family implies F is domains-family ) thus ( F is closed-domains-family implies F is domains-family ) ::_thesis: verum proof assume F is closed-domains-family ; ::_thesis: F is domains-family then A1: F c= Closed_Domains_of T by Th72; Closed_Domains_of T c= Domains_of T by TDLAT_1:31; then F c= Domains_of T by A1, XBOOLE_1:1; hence F is domains-family by Th65; ::_thesis: verum end; end; theorem Th74: :: TDLAT_2:74 for T being non empty TopSpace for F being Subset-Family of T st F is closed-domains-family holds F is closed proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is closed-domains-family holds F is closed let F be Subset-Family of T; ::_thesis: ( F is closed-domains-family implies F is closed ) assume A1: F is closed-domains-family ; ::_thesis: F is closed for A being Subset of T st A in F holds A is closed proof let A be Subset of T; ::_thesis: ( A in F implies A is closed ) assume A in F ; ::_thesis: A is closed then A is closed_condensed by A1, Def3; hence A is closed by TOPS_1:66; ::_thesis: verum end; hence F is closed by TOPS_2:def_2; ::_thesis: verum end; theorem :: TDLAT_2:75 for T being non empty TopSpace for F being Subset-Family of T st F is domains-family holds Cl F is closed-domains-family proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is domains-family holds Cl F is closed-domains-family let F be Subset-Family of T; ::_thesis: ( F is domains-family implies Cl F is closed-domains-family ) assume A1: F is domains-family ; ::_thesis: Cl F is closed-domains-family for A being Subset of T st A in Cl F holds A is closed_condensed proof let A be Subset of T; ::_thesis: ( A in Cl F implies A is closed_condensed ) assume A in Cl F ; ::_thesis: A is closed_condensed then consider P being Subset of T such that A2: A = Cl P and A3: P in F by PCOMPS_1:def_2; reconsider P = P as Subset of T ; P is condensed by A1, A3, Def2; hence A is closed_condensed by A2, TDLAT_1:24; ::_thesis: verum end; hence Cl F is closed-domains-family by Def3; ::_thesis: verum end; theorem Th76: :: TDLAT_2:76 for T being non empty TopSpace for F being Subset-Family of T st F is closed-domains-family holds ( Cl (union F) is closed_condensed & Cl (Int (meet F)) is closed_condensed ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is closed-domains-family holds ( Cl (union F) is closed_condensed & Cl (Int (meet F)) is closed_condensed ) let F be Subset-Family of T; ::_thesis: ( F is closed-domains-family implies ( Cl (union F) is closed_condensed & Cl (Int (meet F)) is closed_condensed ) ) assume F is closed-domains-family ; ::_thesis: ( Cl (union F) is closed_condensed & Cl (Int (meet F)) is closed_condensed ) then F is domains-family by Th73; then Cl (union F) = Cl (Int (Cl (union F))) by Th66; hence Cl (union F) is closed_condensed by TOPS_1:def_7; ::_thesis: Cl (Int (meet F)) is closed_condensed thus Cl (Int (meet F)) is closed_condensed by TDLAT_1:22; ::_thesis: verum end; theorem Th77: :: TDLAT_2:77 for T being non empty TopSpace for F being Subset-Family of T holds ( ( for B being Subset of T st B in F holds B c= Cl (union F) ) & ( for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds B c= A ) holds Cl (union F) c= A ) ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds ( ( for B being Subset of T st B in F holds B c= Cl (union F) ) & ( for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds B c= A ) holds Cl (union F) c= A ) ) let F be Subset-Family of T; ::_thesis: ( ( for B being Subset of T st B in F holds B c= Cl (union F) ) & ( for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds B c= A ) holds Cl (union F) c= A ) ) thus for B being Subset of T st B in F holds B c= Cl (union F) ::_thesis: for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds B c= A ) holds Cl (union F) c= A proof let B be Subset of T; ::_thesis: ( B in F implies B c= Cl (union F) ) assume B in F ; ::_thesis: B c= Cl (union F) then A1: B c= union F by ZFMISC_1:74; union F c= Cl (union F) by PRE_TOPC:18; hence B c= Cl (union F) by A1, XBOOLE_1:1; ::_thesis: verum end; thus for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds B c= A ) holds Cl (union F) c= A ::_thesis: verum proof let A be Subset of T; ::_thesis: ( A is closed_condensed & ( for B being Subset of T st B in F holds B c= A ) implies Cl (union F) c= A ) reconsider A1 = A as Subset of T ; assume A is closed_condensed ; ::_thesis: ( ex B being Subset of T st ( B in F & not B c= A ) or Cl (union F) c= A ) then A2: A1 is closed by TOPS_1:66; assume for B being Subset of T st B in F holds B c= A ; ::_thesis: Cl (union F) c= A then for P being set st P in F holds P c= A ; then union F c= A by ZFMISC_1:76; then Cl (union F) c= Cl A by PRE_TOPC:19; hence Cl (union F) c= A by A2, PRE_TOPC:22; ::_thesis: verum end; end; theorem Th78: :: TDLAT_2:78 for T being non empty TopSpace for F being Subset-Family of T holds ( ( F is closed implies for B being Subset of T st B in F holds Cl (Int (meet F)) c= B ) & ( F = {} or for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= Cl (Int (meet F)) ) ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds ( ( F is closed implies for B being Subset of T st B in F holds Cl (Int (meet F)) c= B ) & ( F = {} or for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= Cl (Int (meet F)) ) ) let F be Subset-Family of T; ::_thesis: ( ( F is closed implies for B being Subset of T st B in F holds Cl (Int (meet F)) c= B ) & ( F = {} or for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= Cl (Int (meet F)) ) ) thus ( F is closed implies for B being Subset of T st B in F holds Cl (Int (meet F)) c= B ) ::_thesis: ( F = {} or for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= Cl (Int (meet F)) ) proof assume F is closed ; ::_thesis: for B being Subset of T st B in F holds Cl (Int (meet F)) c= B then meet F is closed by TOPS_2:22; then A1: Cl (meet F) = meet F by PRE_TOPC:22; let B be Subset of T; ::_thesis: ( B in F implies Cl (Int (meet F)) c= B ) A2: Cl (Int (meet F)) c= Cl (meet F) by PRE_TOPC:19, TOPS_1:16; assume B in F ; ::_thesis: Cl (Int (meet F)) c= B then meet F c= B by SETFAM_1:3; hence Cl (Int (meet F)) c= B by A2, A1, XBOOLE_1:1; ::_thesis: verum end; thus ( F = {} or for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= Cl (Int (meet F)) ) ::_thesis: verum proof assume A3: F <> {} ; ::_thesis: for A being Subset of T st A is closed_condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= Cl (Int (meet F)) let A be Subset of T; ::_thesis: ( A is closed_condensed & ( for B being Subset of T st B in F holds A c= B ) implies A c= Cl (Int (meet F)) ) assume A4: A is closed_condensed ; ::_thesis: ( ex B being Subset of T st ( B in F & not A c= B ) or A c= Cl (Int (meet F)) ) assume for B being Subset of T st B in F holds A c= B ; ::_thesis: A c= Cl (Int (meet F)) then for P being set st P in F holds A c= P ; then A c= meet F by A3, SETFAM_1:5; then A5: Int A c= Int (meet F) by TOPS_1:19; A = Cl (Int A) by A4, TOPS_1:def_7; hence A c= Cl (Int (meet F)) by A5, PRE_TOPC:19; ::_thesis: verum end; end; definition let T be non empty TopSpace; let IT be Subset-Family of T; attrIT is open-domains-family means :Def4: :: TDLAT_2:def 4 for A being Subset of T st A in IT holds A is open_condensed ; end; :: deftheorem Def4 defines open-domains-family TDLAT_2:def_4_:_ for T being non empty TopSpace for IT being Subset-Family of T holds ( IT is open-domains-family iff for A being Subset of T st A in IT holds A is open_condensed ); theorem Th79: :: TDLAT_2:79 for T being non empty TopSpace for F being Subset-Family of T holds ( F c= Open_Domains_of T iff F is open-domains-family ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds ( F c= Open_Domains_of T iff F is open-domains-family ) let F be Subset-Family of T; ::_thesis: ( F c= Open_Domains_of T iff F is open-domains-family ) thus ( F c= Open_Domains_of T implies F is open-domains-family ) ::_thesis: ( F is open-domains-family implies F c= Open_Domains_of T ) proof assume A1: F c= Open_Domains_of T ; ::_thesis: F is open-domains-family now__::_thesis:_for_A_being_Subset_of_T_st_A_in_F_holds_ A_is_open_condensed let A be Subset of T; ::_thesis: ( A in F implies A is open_condensed ) assume A in F ; ::_thesis: A is open_condensed then A in Open_Domains_of T by A1; then A in { P where P is Subset of T : P is open_condensed } by TDLAT_1:def_9; then ex Q being Subset of T st ( Q = A & Q is open_condensed ) ; hence A is open_condensed ; ::_thesis: verum end; hence F is open-domains-family by Def4; ::_thesis: verum end; thus ( F is open-domains-family implies F c= Open_Domains_of T ) ::_thesis: verum proof assume A2: F is open-domains-family ; ::_thesis: F c= Open_Domains_of T for X being set st X in F holds X in Open_Domains_of T proof let X be set ; ::_thesis: ( X in F implies X in Open_Domains_of T ) assume A3: X in F ; ::_thesis: X in Open_Domains_of T then reconsider X0 = X as Subset of T ; X0 is open_condensed by A2, A3, Def4; then X0 in { P where P is Subset of T : P is open_condensed } ; hence X in Open_Domains_of T by TDLAT_1:def_9; ::_thesis: verum end; hence F c= Open_Domains_of T by TARSKI:def_3; ::_thesis: verum end; end; theorem Th80: :: TDLAT_2:80 for T being non empty TopSpace for F being Subset-Family of T st F is open-domains-family holds F is domains-family proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is open-domains-family holds F is domains-family let F be Subset-Family of T; ::_thesis: ( F is open-domains-family implies F is domains-family ) thus ( F is open-domains-family implies F is domains-family ) ::_thesis: verum proof assume F is open-domains-family ; ::_thesis: F is domains-family then A1: F c= Open_Domains_of T by Th79; Open_Domains_of T c= Domains_of T by TDLAT_1:35; then F c= Domains_of T by A1, XBOOLE_1:1; hence F is domains-family by Th65; ::_thesis: verum end; end; theorem Th81: :: TDLAT_2:81 for T being non empty TopSpace for F being Subset-Family of T st F is open-domains-family holds F is open proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is open-domains-family holds F is open let F be Subset-Family of T; ::_thesis: ( F is open-domains-family implies F is open ) assume A1: F is open-domains-family ; ::_thesis: F is open for A being Subset of T st A in F holds A is open proof let A be Subset of T; ::_thesis: ( A in F implies A is open ) assume A in F ; ::_thesis: A is open then A is open_condensed by A1, Def4; hence A is open by TOPS_1:67; ::_thesis: verum end; hence F is open by TOPS_2:def_1; ::_thesis: verum end; theorem :: TDLAT_2:82 for T being non empty TopSpace for F being Subset-Family of T st F is domains-family holds Int F is open-domains-family proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is domains-family holds Int F is open-domains-family let F be Subset-Family of T; ::_thesis: ( F is domains-family implies Int F is open-domains-family ) assume A1: F is domains-family ; ::_thesis: Int F is open-domains-family for A being Subset of T st A in Int F holds A is open_condensed proof let A be Subset of T; ::_thesis: ( A in Int F implies A is open_condensed ) assume A in Int F ; ::_thesis: A is open_condensed then consider P being Subset of T such that A2: A = Int P and A3: P in F by Def1; reconsider P = P as Subset of T ; P is condensed by A1, A3, Def2; hence A is open_condensed by A2, TDLAT_1:25; ::_thesis: verum end; hence Int F is open-domains-family by Def4; ::_thesis: verum end; theorem Th83: :: TDLAT_2:83 for T being non empty TopSpace for F being Subset-Family of T st F is open-domains-family holds ( Int (meet F) is open_condensed & Int (Cl (union F)) is open_condensed ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is open-domains-family holds ( Int (meet F) is open_condensed & Int (Cl (union F)) is open_condensed ) let F be Subset-Family of T; ::_thesis: ( F is open-domains-family implies ( Int (meet F) is open_condensed & Int (Cl (union F)) is open_condensed ) ) assume F is open-domains-family ; ::_thesis: ( Int (meet F) is open_condensed & Int (Cl (union F)) is open_condensed ) then F is domains-family by Th80; then Int (Cl (Int (meet F))) = Int (meet F) by Th67; hence Int (meet F) is open_condensed by TOPS_1:def_8; ::_thesis: Int (Cl (union F)) is open_condensed thus Int (Cl (union F)) is open_condensed by TDLAT_1:23; ::_thesis: verum end; theorem Th84: :: TDLAT_2:84 for T being non empty TopSpace for F being Subset-Family of T holds ( ( F is open implies for B being Subset of T st B in F holds B c= Int (Cl (union F)) ) & ( for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds B c= A ) holds Int (Cl (union F)) c= A ) ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds ( ( F is open implies for B being Subset of T st B in F holds B c= Int (Cl (union F)) ) & ( for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds B c= A ) holds Int (Cl (union F)) c= A ) ) let F be Subset-Family of T; ::_thesis: ( ( F is open implies for B being Subset of T st B in F holds B c= Int (Cl (union F)) ) & ( for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds B c= A ) holds Int (Cl (union F)) c= A ) ) thus ( F is open implies for B being Subset of T st B in F holds B c= Int (Cl (union F)) ) ::_thesis: for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds B c= A ) holds Int (Cl (union F)) c= A proof assume F is open ; ::_thesis: for B being Subset of T st B in F holds B c= Int (Cl (union F)) then union F is open by TOPS_2:19; then A1: Int (union F) = union F by TOPS_1:23; let B be Subset of T; ::_thesis: ( B in F implies B c= Int (Cl (union F)) ) A2: Int (union F) c= Int (Cl (union F)) by PRE_TOPC:18, TOPS_1:19; assume B in F ; ::_thesis: B c= Int (Cl (union F)) then B c= union F by ZFMISC_1:74; hence B c= Int (Cl (union F)) by A2, A1, XBOOLE_1:1; ::_thesis: verum end; thus for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds B c= A ) holds Int (Cl (union F)) c= A ::_thesis: verum proof let A be Subset of T; ::_thesis: ( A is open_condensed & ( for B being Subset of T st B in F holds B c= A ) implies Int (Cl (union F)) c= A ) assume A is open_condensed ; ::_thesis: ( ex B being Subset of T st ( B in F & not B c= A ) or Int (Cl (union F)) c= A ) then A3: A = Int (Cl A) by TOPS_1:def_8; assume for B being Subset of T st B in F holds B c= A ; ::_thesis: Int (Cl (union F)) c= A then for P being set st P in F holds P c= A ; then union F c= A by ZFMISC_1:76; then Cl (union F) c= Cl A by PRE_TOPC:19; hence Int (Cl (union F)) c= A by A3, TOPS_1:19; ::_thesis: verum end; end; theorem Th85: :: TDLAT_2:85 for T being non empty TopSpace for F being Subset-Family of T holds ( ( for B being Subset of T st B in F holds Int (meet F) c= B ) & ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= Int (meet F) ) ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T holds ( ( for B being Subset of T st B in F holds Int (meet F) c= B ) & ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= Int (meet F) ) ) let F be Subset-Family of T; ::_thesis: ( ( for B being Subset of T st B in F holds Int (meet F) c= B ) & ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= Int (meet F) ) ) thus for B being Subset of T st B in F holds Int (meet F) c= B ::_thesis: ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= Int (meet F) ) proof let B be Subset of T; ::_thesis: ( B in F implies Int (meet F) c= B ) assume B in F ; ::_thesis: Int (meet F) c= B then A1: meet F c= B by SETFAM_1:3; Int (meet F) c= meet F by TOPS_1:16; hence Int (meet F) c= B by A1, XBOOLE_1:1; ::_thesis: verum end; thus ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= Int (meet F) ) ::_thesis: verum proof assume A2: F <> {} ; ::_thesis: for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds A c= B ) holds A c= Int (meet F) let A be Subset of T; ::_thesis: ( A is open_condensed & ( for B being Subset of T st B in F holds A c= B ) implies A c= Int (meet F) ) assume A3: A is open_condensed ; ::_thesis: ( ex B being Subset of T st ( B in F & not A c= B ) or A c= Int (meet F) ) assume for B being Subset of T st B in F holds A c= B ; ::_thesis: A c= Int (meet F) then for P being set st P in F holds A c= P ; then A4: A c= meet F by A2, SETFAM_1:5; A is open by A3, TOPS_1:67; then Int A = A by TOPS_1:23; hence A c= Int (meet F) by A4, TOPS_1:19; ::_thesis: verum end; end; begin theorem Th86: :: TDLAT_2:86 for T being non empty TopSpace holds the carrier of (Domains_Lattice T) = Domains_of T proof let T be non empty TopSpace; ::_thesis: the carrier of (Domains_Lattice T) = Domains_of T Domains_Lattice T = LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) by TDLAT_1:def_4; hence the carrier of (Domains_Lattice T) = Domains_of T ; ::_thesis: verum end; theorem Th87: :: TDLAT_2:87 for T being non empty TopSpace for a, b being Element of (Domains_Lattice T) for A, B being Element of Domains_of T st a = A & b = B holds ( a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) & a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) ) proof let T be non empty TopSpace; ::_thesis: for a, b being Element of (Domains_Lattice T) for A, B being Element of Domains_of T st a = A & b = B holds ( a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) & a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) ) let a, b be Element of (Domains_Lattice T); ::_thesis: for A, B being Element of Domains_of T st a = A & b = B holds ( a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) & a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) ) let A, B be Element of Domains_of T; ::_thesis: ( a = A & b = B implies ( a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) & a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) ) ) assume that A1: a = A and A2: b = B ; ::_thesis: ( a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) & a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) ) A3: Domains_Lattice T = LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) by TDLAT_1:def_4; hence a "\/" b = (D-Union T) . (A,B) by A1, A2, LATTICES:def_1 .= (Int (Cl (A \/ B))) \/ (A \/ B) by TDLAT_1:def_2 ; ::_thesis: a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) thus a "/\" b = (D-Meet T) . (A,B) by A3, A1, A2, LATTICES:def_2 .= (Cl (Int (A /\ B))) /\ (A /\ B) by TDLAT_1:def_3 ; ::_thesis: verum end; theorem :: TDLAT_2:88 for T being non empty TopSpace holds ( Bottom (Domains_Lattice T) = {} T & Top (Domains_Lattice T) = [#] T ) proof let T be non empty TopSpace; ::_thesis: ( Bottom (Domains_Lattice T) = {} T & Top (Domains_Lattice T) = [#] T ) thus Bottom (Domains_Lattice T) = {} T ::_thesis: Top (Domains_Lattice T) = [#] T proof {} T is condensed by TDLAT_1:14; then A1: {} T in { A where A is Subset of T : A is condensed } ; then reconsider E = {} T as Element of Domains_of T by TDLAT_1:def_1; {} T in Domains_of T by A1, TDLAT_1:def_1; then reconsider e = {} T as Element of (Domains_Lattice T) by Th86; for a being Element of (Domains_Lattice T) holds e "\/" a = a proof let a be Element of (Domains_Lattice T); ::_thesis: e "\/" a = a reconsider A = a as Element of Domains_of T by Th86; A in Domains_of T ; then A in { C where C is Subset of T : C is condensed } by TDLAT_1:def_1; then ex D being Subset of T st ( D = A & D is condensed ) ; then A2: Int (Cl A) c= A by TOPS_1:def_6; thus e "\/" a = (Int (Cl (E \/ A))) \/ (E \/ A) by Th87 .= a by A2, XBOOLE_1:12 ; ::_thesis: verum end; hence Bottom (Domains_Lattice T) = {} T by LATTICE2:14; ::_thesis: verum end; thus Top (Domains_Lattice T) = [#] T ::_thesis: verum proof [#] T is condensed by TDLAT_1:15; then A3: [#] T in { A where A is Subset of T : A is condensed } ; then reconsider E = [#] T as Element of Domains_of T by TDLAT_1:def_1; [#] T in Domains_of T by A3, TDLAT_1:def_1; then reconsider e = [#] T as Element of (Domains_Lattice T) by Th86; for a being Element of (Domains_Lattice T) holds e "/\" a = a proof let a be Element of (Domains_Lattice T); ::_thesis: e "/\" a = a reconsider A = a as Element of Domains_of T by Th86; A in Domains_of T ; then A in { C where C is Subset of T : C is condensed } by TDLAT_1:def_1; then ex D being Subset of T st ( D = A & D is condensed ) ; then A4: A c= Cl (Int A) by TOPS_1:def_6; thus e "/\" a = (Cl (Int (E /\ A))) /\ (E /\ A) by Th87 .= (Cl (Int A)) /\ (([#] T) /\ A) by XBOOLE_1:28 .= (Cl (Int A)) /\ A by XBOOLE_1:28 .= a by A4, XBOOLE_1:28 ; ::_thesis: verum end; hence Top (Domains_Lattice T) = [#] T by LATTICE2:16; ::_thesis: verum end; end; theorem Th89: :: TDLAT_2:89 for T being non empty TopSpace for a, b being Element of (Domains_Lattice T) for A, B being Element of Domains_of T st a = A & b = B holds ( a [= b iff A c= B ) proof let T be non empty TopSpace; ::_thesis: for a, b being Element of (Domains_Lattice T) for A, B being Element of Domains_of T st a = A & b = B holds ( a [= b iff A c= B ) let a, b be Element of (Domains_Lattice T); ::_thesis: for A, B being Element of Domains_of T st a = A & b = B holds ( a [= b iff A c= B ) let A, B be Element of Domains_of T; ::_thesis: ( a = A & b = B implies ( a [= b iff A c= B ) ) assume that A1: a = A and A2: b = B ; ::_thesis: ( a [= b iff A c= B ) B in Domains_of T ; then B in { C where C is Subset of T : C is condensed } by TDLAT_1:def_1; then A3: ex Q being Subset of T st ( Q = B & Q is condensed ) ; thus ( a [= b implies A c= B ) ::_thesis: ( A c= B implies a [= b ) proof assume a [= b ; ::_thesis: A c= B then a "\/" b = b by LATTICES:def_3; then (Int (Cl (A \/ B))) \/ (A \/ B) = B by A1, A2, Th87; hence A c= B by A3, Th59; ::_thesis: verum end; assume A c= B ; ::_thesis: a [= b then (Int (Cl (A \/ B))) \/ (A \/ B) = B by A3, Th59; then a "\/" b = b by A1, A2, Th87; hence a [= b by LATTICES:def_3; ::_thesis: verum end; theorem Th90: :: TDLAT_2:90 for T being non empty TopSpace for X being Subset of (Domains_Lattice T) ex a being Element of (Domains_Lattice T) st ( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds a [= b ) ) proof let T be non empty TopSpace; ::_thesis: for X being Subset of (Domains_Lattice T) ex a being Element of (Domains_Lattice T) st ( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds a [= b ) ) let X be Subset of (Domains_Lattice T); ::_thesis: ex a being Element of (Domains_Lattice T) st ( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds a [= b ) ) X c= the carrier of (Domains_Lattice T) ; then A1: X c= Domains_of T by Th86; then reconsider F = X as Subset-Family of T by TOPS_2:2; set A = (union F) \/ (Int (Cl (union F))); A2: F is domains-family by A1, Th65; then (union F) \/ (Int (Cl (union F))) is condensed by Th68; then (union F) \/ (Int (Cl (union F))) in { C where C is Subset of T : C is condensed } ; then A3: (union F) \/ (Int (Cl (union F))) in Domains_of T by TDLAT_1:def_1; then reconsider a = (union F) \/ (Int (Cl (union F))) as Element of (Domains_Lattice T) by Th86; A4: for b being Element of (Domains_Lattice T) st X is_less_than b holds a [= b proof let b be Element of (Domains_Lattice T); ::_thesis: ( X is_less_than b implies a [= b ) reconsider B = b as Element of Domains_of T by Th86; assume A5: X is_less_than b ; ::_thesis: a [= b A6: for C being Subset of T st C in F holds C c= B proof let C be Subset of T; ::_thesis: ( C in F implies C c= B ) reconsider C1 = C as Subset of T ; assume A7: C in F ; ::_thesis: C c= B then C1 is condensed by A2, Def2; then C in { P where P is Subset of T : P is condensed } ; then A8: C in Domains_of T by TDLAT_1:def_1; then reconsider c = C as Element of (Domains_Lattice T) by Th86; c [= b by A5, A7, LATTICE3:def_17; hence C c= B by A8, Th89; ::_thesis: verum end; B in Domains_of T ; then B in { C where C is Subset of T : C is condensed } by TDLAT_1:def_1; then ex C being Subset of T st ( C = B & C is condensed ) ; then (union F) \/ (Int (Cl (union F))) c= B by A6, Th69; hence a [= b by A3, Th89; ::_thesis: verum end; take a ; ::_thesis: ( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds a [= b ) ) X is_less_than a proof let b be Element of (Domains_Lattice T); :: according to LATTICE3:def_17 ::_thesis: ( not b in X or b [= a ) reconsider B = b as Element of Domains_of T by Th86; assume b in X ; ::_thesis: b [= a then B c= (union F) \/ (Int (Cl (union F))) by Th69; hence b [= a by A3, Th89; ::_thesis: verum end; hence ( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds a [= b ) ) by A4; ::_thesis: verum end; theorem Th91: :: TDLAT_2:91 for T being non empty TopSpace holds Domains_Lattice T is complete proof let T be non empty TopSpace; ::_thesis: Domains_Lattice T is complete thus for X being set ex a being Element of (Domains_Lattice T) st ( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds a [= b ) ) :: according to LATTICE3:def_18 ::_thesis: verum proof let X be set ; ::_thesis: ex a being Element of (Domains_Lattice T) st ( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds a [= b ) ) set Y = { c where c is Element of (Domains_Lattice T) : c in X } ; A1: for d being Element of (Domains_Lattice T) st { c where c is Element of (Domains_Lattice T) : c in X } is_less_than d holds X is_less_than d proof let d be Element of (Domains_Lattice T); ::_thesis: ( { c where c is Element of (Domains_Lattice T) : c in X } is_less_than d implies X is_less_than d ) assume A2: { c where c is Element of (Domains_Lattice T) : c in X } is_less_than d ; ::_thesis: X is_less_than d thus for e being Element of (Domains_Lattice T) st e in X holds e [= d :: according to LATTICE3:def_17 ::_thesis: verum proof let e be Element of (Domains_Lattice T); ::_thesis: ( e in X implies e [= d ) assume e in X ; ::_thesis: e [= d then e in { c where c is Element of (Domains_Lattice T) : c in X } ; hence e [= d by A2, LATTICE3:def_17; ::_thesis: verum end; end; A3: for d being Element of (Domains_Lattice T) st X is_less_than d holds { c where c is Element of (Domains_Lattice T) : c in X } is_less_than d proof let d be Element of (Domains_Lattice T); ::_thesis: ( X is_less_than d implies { c where c is Element of (Domains_Lattice T) : c in X } is_less_than d ) assume A4: X is_less_than d ; ::_thesis: { c where c is Element of (Domains_Lattice T) : c in X } is_less_than d thus for e being Element of (Domains_Lattice T) st e in { c where c is Element of (Domains_Lattice T) : c in X } holds e [= d :: according to LATTICE3:def_17 ::_thesis: verum proof let e be Element of (Domains_Lattice T); ::_thesis: ( e in { c where c is Element of (Domains_Lattice T) : c in X } implies e [= d ) assume e in { c where c is Element of (Domains_Lattice T) : c in X } ; ::_thesis: e [= d then ex e0 being Element of (Domains_Lattice T) st ( e0 = e & e0 in X ) ; hence e [= d by A4, LATTICE3:def_17; ::_thesis: verum end; end; now__::_thesis:_for_x_being_set_st_x_in__{__c_where_c_is_Element_of_(Domains_Lattice_T)_:_c_in_X__}__holds_ x_in_the_carrier_of_(Domains_Lattice_T) let x be set ; ::_thesis: ( x in { c where c is Element of (Domains_Lattice T) : c in X } implies x in the carrier of (Domains_Lattice T) ) assume x in { c where c is Element of (Domains_Lattice T) : c in X } ; ::_thesis: x in the carrier of (Domains_Lattice T) then ex y being Element of (Domains_Lattice T) st ( y = x & y in X ) ; hence x in the carrier of (Domains_Lattice T) ; ::_thesis: verum end; then reconsider Y = { c where c is Element of (Domains_Lattice T) : c in X } as Subset of (Domains_Lattice T) by TARSKI:def_3; consider a being Element of (Domains_Lattice T) such that A5: Y is_less_than a and A6: for b being Element of (Domains_Lattice T) st Y is_less_than b holds a [= b by Th90; take a ; ::_thesis: ( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds a [= b ) ) for b being Element of (Domains_Lattice T) st X is_less_than b holds a [= b by A3, A6; hence ( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds a [= b ) ) by A1, A5; ::_thesis: verum end; end; theorem Th92: :: TDLAT_2:92 for T being non empty TopSpace for F being Subset-Family of T st F is domains-family holds for X being Subset of (Domains_Lattice T) st X = F holds "\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F))) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is domains-family holds for X being Subset of (Domains_Lattice T) st X = F holds "\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F))) let F be Subset-Family of T; ::_thesis: ( F is domains-family implies for X being Subset of (Domains_Lattice T) st X = F holds "\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F))) ) assume A1: F is domains-family ; ::_thesis: for X being Subset of (Domains_Lattice T) st X = F holds "\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F))) let X be Subset of (Domains_Lattice T); ::_thesis: ( X = F implies "\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F))) ) assume A2: X = F ; ::_thesis: "\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F))) thus "\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F))) ::_thesis: verum proof set A = (union F) \/ (Int (Cl (union F))); (union F) \/ (Int (Cl (union F))) is condensed by A1, Th68; then (union F) \/ (Int (Cl (union F))) in { C where C is Subset of T : C is condensed } ; then A3: (union F) \/ (Int (Cl (union F))) in Domains_of T by TDLAT_1:def_1; then reconsider a = (union F) \/ (Int (Cl (union F))) as Element of (Domains_Lattice T) by Th86; A4: X is_less_than a proof let b be Element of (Domains_Lattice T); :: according to LATTICE3:def_17 ::_thesis: ( not b in X or b [= a ) reconsider B = b as Element of Domains_of T by Th86; assume b in X ; ::_thesis: b [= a then B c= (union F) \/ (Int (Cl (union F))) by A2, Th69; hence b [= a by A3, Th89; ::_thesis: verum end; A5: for b being Element of (Domains_Lattice T) st X is_less_than b holds a [= b proof let b be Element of (Domains_Lattice T); ::_thesis: ( X is_less_than b implies a [= b ) reconsider B = b as Element of Domains_of T by Th86; assume A6: X is_less_than b ; ::_thesis: a [= b A7: for C being Subset of T st C in F holds C c= B proof let C be Subset of T; ::_thesis: ( C in F implies C c= B ) reconsider C1 = C as Subset of T ; assume A8: C in F ; ::_thesis: C c= B then C1 is condensed by A1, Def2; then C in { P where P is Subset of T : P is condensed } ; then A9: C in Domains_of T by TDLAT_1:def_1; then reconsider c = C as Element of (Domains_Lattice T) by Th86; c [= b by A2, A6, A8, LATTICE3:def_17; hence C c= B by A9, Th89; ::_thesis: verum end; B in Domains_of T ; then B in { C where C is Subset of T : C is condensed } by TDLAT_1:def_1; then ex C being Subset of T st ( C = B & C is condensed ) ; then (union F) \/ (Int (Cl (union F))) c= B by A7, Th69; hence a [= b by A3, Th89; ::_thesis: verum end; Domains_Lattice T is complete by Th91; hence "\/" (X,(Domains_Lattice T)) = (union F) \/ (Int (Cl (union F))) by A4, A5, LATTICE3:def_21; ::_thesis: verum end; end; theorem Th93: :: TDLAT_2:93 for T being non empty TopSpace for F being Subset-Family of T st F is domains-family holds for X being Subset of (Domains_Lattice T) st X = F holds ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is domains-family holds for X being Subset of (Domains_Lattice T) st X = F holds ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) let F be Subset-Family of T; ::_thesis: ( F is domains-family implies for X being Subset of (Domains_Lattice T) st X = F holds ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) ) assume A1: F is domains-family ; ::_thesis: for X being Subset of (Domains_Lattice T) st X = F holds ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) let X be Subset of (Domains_Lattice T); ::_thesis: ( X = F implies ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) ) assume A2: X = F ; ::_thesis: ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) thus ( X <> {} implies "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) ) ::_thesis: ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) proof set A = (meet F) /\ (Cl (Int (meet F))); (meet F) /\ (Cl (Int (meet F))) is condensed by A1, Th70; then (meet F) /\ (Cl (Int (meet F))) in { C where C is Subset of T : C is condensed } ; then A3: (meet F) /\ (Cl (Int (meet F))) in Domains_of T by TDLAT_1:def_1; then reconsider a = (meet F) /\ (Cl (Int (meet F))) as Element of (Domains_Lattice T) by Th86; A4: a is_less_than X proof let b be Element of (Domains_Lattice T); :: according to LATTICE3:def_16 ::_thesis: ( not b in X or a [= b ) reconsider B = b as Element of Domains_of T by Th86; assume b in X ; ::_thesis: a [= b then (meet F) /\ (Cl (Int (meet F))) c= B by A2, Th71; hence a [= b by A3, Th89; ::_thesis: verum end; assume A5: X <> {} ; ::_thesis: "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) A6: for b being Element of (Domains_Lattice T) st b is_less_than X holds b [= a proof let b be Element of (Domains_Lattice T); ::_thesis: ( b is_less_than X implies b [= a ) reconsider B = b as Element of Domains_of T by Th86; assume A7: b is_less_than X ; ::_thesis: b [= a A8: for C being Subset of T st C in F holds B c= C proof let C be Subset of T; ::_thesis: ( C in F implies B c= C ) reconsider C1 = C as Subset of T ; assume A9: C in F ; ::_thesis: B c= C then C1 is condensed by A1, Def2; then C in { P where P is Subset of T : P is condensed } ; then A10: C in Domains_of T by TDLAT_1:def_1; then reconsider c = C as Element of (Domains_Lattice T) by Th86; b [= c by A2, A7, A9, LATTICE3:def_16; hence B c= C by A10, Th89; ::_thesis: verum end; B in Domains_of T ; then B in { C where C is Subset of T : C is condensed } by TDLAT_1:def_1; then ex C being Subset of T st ( C = B & C is condensed ) ; then B c= (meet F) /\ (Cl (Int (meet F))) by A2, A5, A8, Th71; hence b [= a by A3, Th89; ::_thesis: verum end; Domains_Lattice T is complete by Th91; hence "/\" (X,(Domains_Lattice T)) = (meet F) /\ (Cl (Int (meet F))) by A4, A6, LATTICE3:34; ::_thesis: verum end; thus ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ::_thesis: verum proof set A = [#] T; [#] T is condensed by TDLAT_1:15; then [#] T in { C where C is Subset of T : C is condensed } ; then A11: [#] T in Domains_of T by TDLAT_1:def_1; then reconsider a = [#] T as Element of (Domains_Lattice T) by Th86; A12: for b being Element of (Domains_Lattice T) st b is_less_than X holds b [= a proof let b be Element of (Domains_Lattice T); ::_thesis: ( b is_less_than X implies b [= a ) reconsider B = b as Element of Domains_of T by Th86; assume b is_less_than X ; ::_thesis: b [= a B c= [#] T ; hence b [= a by A11, Th89; ::_thesis: verum end; assume A13: X = {} ; ::_thesis: "/\" (X,(Domains_Lattice T)) = [#] T A14: a is_less_than X proof let b be Element of (Domains_Lattice T); :: according to LATTICE3:def_16 ::_thesis: ( not b in X or a [= b ) assume b in X ; ::_thesis: a [= b hence a [= b by A13; ::_thesis: verum end; Domains_Lattice T is complete by Th91; hence "/\" (X,(Domains_Lattice T)) = [#] T by A14, A12, LATTICE3:34; ::_thesis: verum end; end; begin theorem Th94: :: TDLAT_2:94 for T being non empty TopSpace holds the carrier of (Closed_Domains_Lattice T) = Closed_Domains_of T proof let T be non empty TopSpace; ::_thesis: the carrier of (Closed_Domains_Lattice T) = Closed_Domains_of T Closed_Domains_Lattice T = LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) by TDLAT_1:def_8; hence the carrier of (Closed_Domains_Lattice T) = Closed_Domains_of T ; ::_thesis: verum end; theorem Th95: :: TDLAT_2:95 for T being non empty TopSpace for a, b being Element of (Closed_Domains_Lattice T) for A, B being Element of Closed_Domains_of T st a = A & b = B holds ( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) ) proof let T be non empty TopSpace; ::_thesis: for a, b being Element of (Closed_Domains_Lattice T) for A, B being Element of Closed_Domains_of T st a = A & b = B holds ( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) ) let a, b be Element of (Closed_Domains_Lattice T); ::_thesis: for A, B being Element of Closed_Domains_of T st a = A & b = B holds ( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) ) let A, B be Element of Closed_Domains_of T; ::_thesis: ( a = A & b = B implies ( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) ) ) assume that A1: a = A and A2: b = B ; ::_thesis: ( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) ) A3: Closed_Domains_Lattice T = LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) by TDLAT_1:def_8; hence a "\/" b = (CLD-Union T) . (A,B) by A1, A2, LATTICES:def_1 .= A \/ B by TDLAT_1:def_6 ; ::_thesis: a "/\" b = Cl (Int (A /\ B)) thus a "/\" b = (CLD-Meet T) . (A,B) by A3, A1, A2, LATTICES:def_2 .= Cl (Int (A /\ B)) by TDLAT_1:def_7 ; ::_thesis: verum end; theorem :: TDLAT_2:96 for T being non empty TopSpace holds ( Bottom (Closed_Domains_Lattice T) = {} T & Top (Closed_Domains_Lattice T) = [#] T ) proof let T be non empty TopSpace; ::_thesis: ( Bottom (Closed_Domains_Lattice T) = {} T & Top (Closed_Domains_Lattice T) = [#] T ) thus Bottom (Closed_Domains_Lattice T) = {} T ::_thesis: Top (Closed_Domains_Lattice T) = [#] T proof {} T is closed_condensed by TDLAT_1:18; then A1: {} T in { A where A is Subset of T : A is closed_condensed } ; then reconsider E = {} T as Element of Closed_Domains_of T by TDLAT_1:def_5; {} T in Closed_Domains_of T by A1, TDLAT_1:def_5; then reconsider e = {} T as Element of (Closed_Domains_Lattice T) by Th94; for a being Element of (Closed_Domains_Lattice T) holds e "\/" a = a proof let a be Element of (Closed_Domains_Lattice T); ::_thesis: e "\/" a = a reconsider A = a as Element of Closed_Domains_of T by Th94; thus e "\/" a = E \/ A by Th95 .= a ; ::_thesis: verum end; hence Bottom (Closed_Domains_Lattice T) = {} T by LATTICE2:14; ::_thesis: verum end; thus Top (Closed_Domains_Lattice T) = [#] T ::_thesis: verum proof [#] T is closed_condensed by TDLAT_1:19; then A2: [#] T in { A where A is Subset of T : A is closed_condensed } ; then reconsider E = [#] T as Element of Closed_Domains_of T by TDLAT_1:def_5; [#] T in Closed_Domains_of T by A2, TDLAT_1:def_5; then reconsider e = [#] T as Element of (Closed_Domains_Lattice T) by Th94; for a being Element of (Closed_Domains_Lattice T) holds e "/\" a = a proof let a be Element of (Closed_Domains_Lattice T); ::_thesis: e "/\" a = a reconsider A = a as Element of Closed_Domains_of T by Th94; A in Closed_Domains_of T ; then A in { C where C is Subset of T : C is closed_condensed } by TDLAT_1:def_5; then A3: ex D being Subset of T st ( D = A & D is closed_condensed ) ; thus e "/\" a = Cl (Int (E /\ A)) by Th95 .= Cl (Int A) by XBOOLE_1:28 .= a by A3, TOPS_1:def_7 ; ::_thesis: verum end; hence Top (Closed_Domains_Lattice T) = [#] T by LATTICE2:16; ::_thesis: verum end; end; theorem Th97: :: TDLAT_2:97 for T being non empty TopSpace for a, b being Element of (Closed_Domains_Lattice T) for A, B being Element of Closed_Domains_of T st a = A & b = B holds ( a [= b iff A c= B ) proof let T be non empty TopSpace; ::_thesis: for a, b being Element of (Closed_Domains_Lattice T) for A, B being Element of Closed_Domains_of T st a = A & b = B holds ( a [= b iff A c= B ) let a, b be Element of (Closed_Domains_Lattice T); ::_thesis: for A, B being Element of Closed_Domains_of T st a = A & b = B holds ( a [= b iff A c= B ) let A, B be Element of Closed_Domains_of T; ::_thesis: ( a = A & b = B implies ( a [= b iff A c= B ) ) assume that A1: a = A and A2: b = B ; ::_thesis: ( a [= b iff A c= B ) thus ( a [= b implies A c= B ) ::_thesis: ( A c= B implies a [= b ) proof assume a [= b ; ::_thesis: A c= B then a "\/" b = b by LATTICES:def_3; then A \/ B = B by A1, A2, Th95; hence A c= B by XBOOLE_1:7; ::_thesis: verum end; thus ( A c= B implies a [= b ) ::_thesis: verum proof assume A c= B ; ::_thesis: a [= b then A \/ B = B by XBOOLE_1:12; then a "\/" b = b by A1, A2, Th95; hence a [= b by LATTICES:def_3; ::_thesis: verum end; end; theorem Th98: :: TDLAT_2:98 for T being non empty TopSpace for X being Subset of (Closed_Domains_Lattice T) ex a being Element of (Closed_Domains_Lattice T) st ( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds a [= b ) ) proof let T be non empty TopSpace; ::_thesis: for X being Subset of (Closed_Domains_Lattice T) ex a being Element of (Closed_Domains_Lattice T) st ( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds a [= b ) ) let X be Subset of (Closed_Domains_Lattice T); ::_thesis: ex a being Element of (Closed_Domains_Lattice T) st ( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds a [= b ) ) X c= the carrier of (Closed_Domains_Lattice T) ; then A1: X c= Closed_Domains_of T by Th94; then reconsider F = X as Subset-Family of T by TOPS_2:2; set A = Cl (union F); A2: F is closed-domains-family by A1, Th72; then Cl (union F) is closed_condensed by Th76; then Cl (union F) in { C where C is Subset of T : C is closed_condensed } ; then A3: Cl (union F) in Closed_Domains_of T by TDLAT_1:def_5; then reconsider a = Cl (union F) as Element of (Closed_Domains_Lattice T) by Th94; A4: for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds a [= b proof let b be Element of (Closed_Domains_Lattice T); ::_thesis: ( X is_less_than b implies a [= b ) reconsider B = b as Element of Closed_Domains_of T by Th94; assume A5: X is_less_than b ; ::_thesis: a [= b A6: for C being Subset of T st C in F holds C c= B proof let C be Subset of T; ::_thesis: ( C in F implies C c= B ) reconsider C1 = C as Subset of T ; assume A7: C in F ; ::_thesis: C c= B then C1 is closed_condensed by A2, Def3; then C in { P where P is Subset of T : P is closed_condensed } ; then A8: C in Closed_Domains_of T by TDLAT_1:def_5; then reconsider c = C as Element of (Closed_Domains_Lattice T) by Th94; c [= b by A5, A7, LATTICE3:def_17; hence C c= B by A8, Th97; ::_thesis: verum end; B in Closed_Domains_of T ; then B in { C where C is Subset of T : C is closed_condensed } by TDLAT_1:def_5; then ex C being Subset of T st ( C = B & C is closed_condensed ) ; then Cl (union F) c= B by A6, Th77; hence a [= b by A3, Th97; ::_thesis: verum end; take a ; ::_thesis: ( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds a [= b ) ) X is_less_than a proof let b be Element of (Closed_Domains_Lattice T); :: according to LATTICE3:def_17 ::_thesis: ( not b in X or b [= a ) reconsider B = b as Element of Closed_Domains_of T by Th94; assume b in X ; ::_thesis: b [= a then B c= Cl (union F) by Th77; hence b [= a by A3, Th97; ::_thesis: verum end; hence ( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds a [= b ) ) by A4; ::_thesis: verum end; theorem Th99: :: TDLAT_2:99 for T being non empty TopSpace holds Closed_Domains_Lattice T is complete proof let T be non empty TopSpace; ::_thesis: Closed_Domains_Lattice T is complete thus for X being set ex a being Element of (Closed_Domains_Lattice T) st ( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds a [= b ) ) :: according to LATTICE3:def_18 ::_thesis: verum proof let X be set ; ::_thesis: ex a being Element of (Closed_Domains_Lattice T) st ( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds a [= b ) ) set Y = { c where c is Element of (Closed_Domains_Lattice T) : c in X } ; A1: for d being Element of (Closed_Domains_Lattice T) st { c where c is Element of (Closed_Domains_Lattice T) : c in X } is_less_than d holds X is_less_than d proof let d be Element of (Closed_Domains_Lattice T); ::_thesis: ( { c where c is Element of (Closed_Domains_Lattice T) : c in X } is_less_than d implies X is_less_than d ) assume A2: { c where c is Element of (Closed_Domains_Lattice T) : c in X } is_less_than d ; ::_thesis: X is_less_than d thus for e being Element of (Closed_Domains_Lattice T) st e in X holds e [= d :: according to LATTICE3:def_17 ::_thesis: verum proof let e be Element of (Closed_Domains_Lattice T); ::_thesis: ( e in X implies e [= d ) assume e in X ; ::_thesis: e [= d then e in { c where c is Element of (Closed_Domains_Lattice T) : c in X } ; hence e [= d by A2, LATTICE3:def_17; ::_thesis: verum end; end; A3: for d being Element of (Closed_Domains_Lattice T) st X is_less_than d holds { c where c is Element of (Closed_Domains_Lattice T) : c in X } is_less_than d proof let d be Element of (Closed_Domains_Lattice T); ::_thesis: ( X is_less_than d implies { c where c is Element of (Closed_Domains_Lattice T) : c in X } is_less_than d ) assume A4: X is_less_than d ; ::_thesis: { c where c is Element of (Closed_Domains_Lattice T) : c in X } is_less_than d thus for e being Element of (Closed_Domains_Lattice T) st e in { c where c is Element of (Closed_Domains_Lattice T) : c in X } holds e [= d :: according to LATTICE3:def_17 ::_thesis: verum proof let e be Element of (Closed_Domains_Lattice T); ::_thesis: ( e in { c where c is Element of (Closed_Domains_Lattice T) : c in X } implies e [= d ) assume e in { c where c is Element of (Closed_Domains_Lattice T) : c in X } ; ::_thesis: e [= d then ex e0 being Element of (Closed_Domains_Lattice T) st ( e0 = e & e0 in X ) ; hence e [= d by A4, LATTICE3:def_17; ::_thesis: verum end; end; now__::_thesis:_for_x_being_set_st_x_in__{__c_where_c_is_Element_of_(Closed_Domains_Lattice_T)_:_c_in_X__}__holds_ x_in_the_carrier_of_(Closed_Domains_Lattice_T) let x be set ; ::_thesis: ( x in { c where c is Element of (Closed_Domains_Lattice T) : c in X } implies x in the carrier of (Closed_Domains_Lattice T) ) assume x in { c where c is Element of (Closed_Domains_Lattice T) : c in X } ; ::_thesis: x in the carrier of (Closed_Domains_Lattice T) then ex y being Element of (Closed_Domains_Lattice T) st ( y = x & y in X ) ; hence x in the carrier of (Closed_Domains_Lattice T) ; ::_thesis: verum end; then reconsider Y = { c where c is Element of (Closed_Domains_Lattice T) : c in X } as Subset of (Closed_Domains_Lattice T) by TARSKI:def_3; consider a being Element of (Closed_Domains_Lattice T) such that A5: Y is_less_than a and A6: for b being Element of (Closed_Domains_Lattice T) st Y is_less_than b holds a [= b by Th98; take a ; ::_thesis: ( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds a [= b ) ) for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds a [= b by A3, A6; hence ( X is_less_than a & ( for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds a [= b ) ) by A1, A5; ::_thesis: verum end; end; theorem :: TDLAT_2:100 for T being non empty TopSpace for F being Subset-Family of T st F is closed-domains-family holds for X being Subset of (Closed_Domains_Lattice T) st X = F holds "\/" (X,(Closed_Domains_Lattice T)) = Cl (union F) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is closed-domains-family holds for X being Subset of (Closed_Domains_Lattice T) st X = F holds "\/" (X,(Closed_Domains_Lattice T)) = Cl (union F) let F be Subset-Family of T; ::_thesis: ( F is closed-domains-family implies for X being Subset of (Closed_Domains_Lattice T) st X = F holds "\/" (X,(Closed_Domains_Lattice T)) = Cl (union F) ) assume A1: F is closed-domains-family ; ::_thesis: for X being Subset of (Closed_Domains_Lattice T) st X = F holds "\/" (X,(Closed_Domains_Lattice T)) = Cl (union F) let X be Subset of (Closed_Domains_Lattice T); ::_thesis: ( X = F implies "\/" (X,(Closed_Domains_Lattice T)) = Cl (union F) ) assume A2: X = F ; ::_thesis: "\/" (X,(Closed_Domains_Lattice T)) = Cl (union F) thus "\/" (X,(Closed_Domains_Lattice T)) = Cl (union F) ::_thesis: verum proof set A = Cl (union F); Cl (union F) is closed_condensed by A1, Th76; then Cl (union F) in { C where C is Subset of T : C is closed_condensed } ; then A3: Cl (union F) in Closed_Domains_of T by TDLAT_1:def_5; then reconsider a = Cl (union F) as Element of (Closed_Domains_Lattice T) by Th94; A4: X is_less_than a proof let b be Element of (Closed_Domains_Lattice T); :: according to LATTICE3:def_17 ::_thesis: ( not b in X or b [= a ) reconsider B = b as Element of Closed_Domains_of T by Th94; assume b in X ; ::_thesis: b [= a then B c= Cl (union F) by A2, Th77; hence b [= a by A3, Th97; ::_thesis: verum end; A5: for b being Element of (Closed_Domains_Lattice T) st X is_less_than b holds a [= b proof let b be Element of (Closed_Domains_Lattice T); ::_thesis: ( X is_less_than b implies a [= b ) reconsider B = b as Element of Closed_Domains_of T by Th94; assume A6: X is_less_than b ; ::_thesis: a [= b A7: for C being Subset of T st C in F holds C c= B proof let C be Subset of T; ::_thesis: ( C in F implies C c= B ) reconsider C1 = C as Subset of T ; assume A8: C in F ; ::_thesis: C c= B then C1 is closed_condensed by A1, Def3; then C in { P where P is Subset of T : P is closed_condensed } ; then A9: C in Closed_Domains_of T by TDLAT_1:def_5; then reconsider c = C as Element of (Closed_Domains_Lattice T) by Th94; c [= b by A2, A6, A8, LATTICE3:def_17; hence C c= B by A9, Th97; ::_thesis: verum end; B in Closed_Domains_of T ; then B in { C where C is Subset of T : C is closed_condensed } by TDLAT_1:def_5; then ex C being Subset of T st ( C = B & C is closed_condensed ) ; then Cl (union F) c= B by A7, Th77; hence a [= b by A3, Th97; ::_thesis: verum end; Closed_Domains_Lattice T is complete by Th99; hence "\/" (X,(Closed_Domains_Lattice T)) = Cl (union F) by A4, A5, LATTICE3:def_21; ::_thesis: verum end; end; theorem :: TDLAT_2:101 for T being non empty TopSpace for F being Subset-Family of T st F is closed-domains-family holds for X being Subset of (Closed_Domains_Lattice T) st X = F holds ( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is closed-domains-family holds for X being Subset of (Closed_Domains_Lattice T) st X = F holds ( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) ) let F be Subset-Family of T; ::_thesis: ( F is closed-domains-family implies for X being Subset of (Closed_Domains_Lattice T) st X = F holds ( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) ) ) assume A1: F is closed-domains-family ; ::_thesis: for X being Subset of (Closed_Domains_Lattice T) st X = F holds ( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) ) let X be Subset of (Closed_Domains_Lattice T); ::_thesis: ( X = F implies ( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) ) ) assume A2: X = F ; ::_thesis: ( ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) ) thus ( X <> {} implies "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) ) ::_thesis: ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) proof set A = Cl (Int (meet F)); Cl (Int (meet F)) is closed_condensed by A1, Th76; then Cl (Int (meet F)) in { C where C is Subset of T : C is closed_condensed } ; then A3: Cl (Int (meet F)) in Closed_Domains_of T by TDLAT_1:def_5; then reconsider a = Cl (Int (meet F)) as Element of (Closed_Domains_Lattice T) by Th94; A4: a is_less_than X proof let b be Element of (Closed_Domains_Lattice T); :: according to LATTICE3:def_16 ::_thesis: ( not b in X or a [= b ) reconsider B = b as Element of Closed_Domains_of T by Th94; assume b in X ; ::_thesis: a [= b then Cl (Int (meet F)) c= B by A1, A2, Th74, Th78; hence a [= b by A3, Th97; ::_thesis: verum end; assume A5: X <> {} ; ::_thesis: "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) A6: for b being Element of (Closed_Domains_Lattice T) st b is_less_than X holds b [= a proof let b be Element of (Closed_Domains_Lattice T); ::_thesis: ( b is_less_than X implies b [= a ) reconsider B = b as Element of Closed_Domains_of T by Th94; assume A7: b is_less_than X ; ::_thesis: b [= a A8: for C being Subset of T st C in F holds B c= C proof let C be Subset of T; ::_thesis: ( C in F implies B c= C ) reconsider C1 = C as Subset of T ; assume A9: C in F ; ::_thesis: B c= C then C1 is closed_condensed by A1, Def3; then C in { P where P is Subset of T : P is closed_condensed } ; then A10: C in Closed_Domains_of T by TDLAT_1:def_5; then reconsider c = C as Element of (Closed_Domains_Lattice T) by Th94; b [= c by A2, A7, A9, LATTICE3:def_16; hence B c= C by A10, Th97; ::_thesis: verum end; B in Closed_Domains_of T ; then B in { C where C is Subset of T : C is closed_condensed } by TDLAT_1:def_5; then ex C being Subset of T st ( C = B & C is closed_condensed ) ; then B c= Cl (Int (meet F)) by A2, A5, A8, Th78; hence b [= a by A3, Th97; ::_thesis: verum end; Closed_Domains_Lattice T is complete by Th99; hence "/\" (X,(Closed_Domains_Lattice T)) = Cl (Int (meet F)) by A4, A6, LATTICE3:34; ::_thesis: verum end; thus ( X = {} implies "/\" (X,(Closed_Domains_Lattice T)) = [#] T ) ::_thesis: verum proof set A = [#] T; [#] T is closed_condensed by TDLAT_1:19; then [#] T in { C where C is Subset of T : C is closed_condensed } ; then A11: [#] T in Closed_Domains_of T by TDLAT_1:def_5; then reconsider a = [#] T as Element of (Closed_Domains_Lattice T) by Th94; A12: for b being Element of (Closed_Domains_Lattice T) st b is_less_than X holds b [= a proof let b be Element of (Closed_Domains_Lattice T); ::_thesis: ( b is_less_than X implies b [= a ) reconsider B = b as Element of Closed_Domains_of T by Th94; assume b is_less_than X ; ::_thesis: b [= a B c= [#] T ; hence b [= a by A11, Th97; ::_thesis: verum end; assume A13: X = {} ; ::_thesis: "/\" (X,(Closed_Domains_Lattice T)) = [#] T A14: a is_less_than X proof let b be Element of (Closed_Domains_Lattice T); :: according to LATTICE3:def_16 ::_thesis: ( not b in X or a [= b ) assume b in X ; ::_thesis: a [= b hence a [= b by A13; ::_thesis: verum end; Closed_Domains_Lattice T is complete by Th99; hence "/\" (X,(Closed_Domains_Lattice T)) = [#] T by A14, A12, LATTICE3:34; ::_thesis: verum end; end; theorem :: TDLAT_2:102 for T being non empty TopSpace for F being Subset-Family of T st F is closed-domains-family holds for X being Subset of (Domains_Lattice T) st X = F holds ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is closed-domains-family holds for X being Subset of (Domains_Lattice T) st X = F holds ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) let F be Subset-Family of T; ::_thesis: ( F is closed-domains-family implies for X being Subset of (Domains_Lattice T) st X = F holds ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) ) A1: Cl (Int (meet F)) c= Cl (meet F) by PRE_TOPC:19, TOPS_1:16; assume A2: F is closed-domains-family ; ::_thesis: for X being Subset of (Domains_Lattice T) st X = F holds ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) then A3: F is domains-family by Th73; let X be Subset of (Domains_Lattice T); ::_thesis: ( X = F implies ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) ) assume A4: X = F ; ::_thesis: ( ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) & ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) ) meet F is closed by A2, Th74, TOPS_2:22; then Cl (Int (meet F)) c= meet F by A1, PRE_TOPC:22; then (meet F) /\ (Cl (Int (meet F))) = Cl (Int (meet F)) by XBOOLE_1:28; hence ( X <> {} implies "/\" (X,(Domains_Lattice T)) = Cl (Int (meet F)) ) by A3, A4, Th93; ::_thesis: ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) thus ( X = {} implies "/\" (X,(Domains_Lattice T)) = [#] T ) by A3, A4, Th93; ::_thesis: verum end; theorem Th103: :: TDLAT_2:103 for T being non empty TopSpace holds the carrier of (Open_Domains_Lattice T) = Open_Domains_of T proof let T be non empty TopSpace; ::_thesis: the carrier of (Open_Domains_Lattice T) = Open_Domains_of T Open_Domains_Lattice T = LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) by TDLAT_1:def_12; hence the carrier of (Open_Domains_Lattice T) = Open_Domains_of T ; ::_thesis: verum end; theorem Th104: :: TDLAT_2:104 for T being non empty TopSpace for a, b being Element of (Open_Domains_Lattice T) for A, B being Element of Open_Domains_of T st a = A & b = B holds ( a "\/" b = Int (Cl (A \/ B)) & a "/\" b = A /\ B ) proof let T be non empty TopSpace; ::_thesis: for a, b being Element of (Open_Domains_Lattice T) for A, B being Element of Open_Domains_of T st a = A & b = B holds ( a "\/" b = Int (Cl (A \/ B)) & a "/\" b = A /\ B ) let a, b be Element of (Open_Domains_Lattice T); ::_thesis: for A, B being Element of Open_Domains_of T st a = A & b = B holds ( a "\/" b = Int (Cl (A \/ B)) & a "/\" b = A /\ B ) let A, B be Element of Open_Domains_of T; ::_thesis: ( a = A & b = B implies ( a "\/" b = Int (Cl (A \/ B)) & a "/\" b = A /\ B ) ) assume that A1: a = A and A2: b = B ; ::_thesis: ( a "\/" b = Int (Cl (A \/ B)) & a "/\" b = A /\ B ) A3: Open_Domains_Lattice T = LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) by TDLAT_1:def_12; hence a "\/" b = (OPD-Union T) . (A,B) by A1, A2, LATTICES:def_1 .= Int (Cl (A \/ B)) by TDLAT_1:def_10 ; ::_thesis: a "/\" b = A /\ B thus a "/\" b = (OPD-Meet T) . (A,B) by A3, A1, A2, LATTICES:def_2 .= A /\ B by TDLAT_1:def_11 ; ::_thesis: verum end; theorem :: TDLAT_2:105 for T being non empty TopSpace holds ( Bottom (Open_Domains_Lattice T) = {} T & Top (Open_Domains_Lattice T) = [#] T ) proof let T be non empty TopSpace; ::_thesis: ( Bottom (Open_Domains_Lattice T) = {} T & Top (Open_Domains_Lattice T) = [#] T ) thus Bottom (Open_Domains_Lattice T) = {} T ::_thesis: Top (Open_Domains_Lattice T) = [#] T proof {} T is open_condensed by TDLAT_1:20; then A1: {} T in { A where A is Subset of T : A is open_condensed } ; then reconsider E = {} T as Element of Open_Domains_of T by TDLAT_1:def_9; {} T in Open_Domains_of T by A1, TDLAT_1:def_9; then reconsider e = {} T as Element of (Open_Domains_Lattice T) by Th103; for a being Element of (Open_Domains_Lattice T) holds e "\/" a = a proof let a be Element of (Open_Domains_Lattice T); ::_thesis: e "\/" a = a reconsider A = a as Element of Open_Domains_of T by Th103; A in Open_Domains_of T ; then A in { C where C is Subset of T : C is open_condensed } by TDLAT_1:def_9; then A2: ex D being Subset of T st ( D = A & D is open_condensed ) ; thus e "\/" a = Int (Cl (E \/ A)) by Th104 .= a by A2, TOPS_1:def_8 ; ::_thesis: verum end; hence Bottom (Open_Domains_Lattice T) = {} T by LATTICE2:14; ::_thesis: verum end; thus Top (Open_Domains_Lattice T) = [#] T ::_thesis: verum proof [#] T is open_condensed by TDLAT_1:21; then A3: [#] T in { A where A is Subset of T : A is open_condensed } ; then reconsider E = [#] T as Element of Open_Domains_of T by TDLAT_1:def_9; [#] T in Open_Domains_of T by A3, TDLAT_1:def_9; then reconsider e = [#] T as Element of (Open_Domains_Lattice T) by Th103; for a being Element of (Open_Domains_Lattice T) holds e "/\" a = a proof let a be Element of (Open_Domains_Lattice T); ::_thesis: e "/\" a = a reconsider A = a as Element of Open_Domains_of T by Th103; thus e "/\" a = E /\ A by Th104 .= a by XBOOLE_1:28 ; ::_thesis: verum end; hence Top (Open_Domains_Lattice T) = [#] T by LATTICE2:16; ::_thesis: verum end; end; theorem Th106: :: TDLAT_2:106 for T being non empty TopSpace for a, b being Element of (Open_Domains_Lattice T) for A, B being Element of Open_Domains_of T st a = A & b = B holds ( a [= b iff A c= B ) proof let T be non empty TopSpace; ::_thesis: for a, b being Element of (Open_Domains_Lattice T) for A, B being Element of Open_Domains_of T st a = A & b = B holds ( a [= b iff A c= B ) let a, b be Element of (Open_Domains_Lattice T); ::_thesis: for A, B being Element of Open_Domains_of T st a = A & b = B holds ( a [= b iff A c= B ) let A, B be Element of Open_Domains_of T; ::_thesis: ( a = A & b = B implies ( a [= b iff A c= B ) ) reconsider A1 = A as Subset of T ; assume that A1: a = A and A2: b = B ; ::_thesis: ( a [= b iff A c= B ) A in Open_Domains_of T ; then A in { C where C is Subset of T : C is open_condensed } by TDLAT_1:def_9; then ex Q being Subset of T st ( Q = A & Q is open_condensed ) ; then A3: A1 is open by TOPS_1:67; thus ( a [= b implies A c= B ) ::_thesis: ( A c= B implies a [= b ) proof assume a [= b ; ::_thesis: A c= B then a "\/" b = b by LATTICES:def_3; then Int (Cl (A \/ B)) = B by A1, A2, Th104; hence A c= B by A3, Th4; ::_thesis: verum end; B in Open_Domains_of T ; then B in { C where C is Subset of T : C is open_condensed } by TDLAT_1:def_9; then A4: ex P being Subset of T st ( P = B & P is open_condensed ) ; thus ( A c= B implies a [= b ) ::_thesis: verum proof assume A c= B ; ::_thesis: a [= b then Int (Cl (A \/ B)) = B by A4, Th64; then a "\/" b = b by A1, A2, Th104; hence a [= b by LATTICES:def_3; ::_thesis: verum end; end; theorem Th107: :: TDLAT_2:107 for T being non empty TopSpace for X being Subset of (Open_Domains_Lattice T) ex a being Element of (Open_Domains_Lattice T) st ( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds a [= b ) ) proof let T be non empty TopSpace; ::_thesis: for X being Subset of (Open_Domains_Lattice T) ex a being Element of (Open_Domains_Lattice T) st ( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds a [= b ) ) let X be Subset of (Open_Domains_Lattice T); ::_thesis: ex a being Element of (Open_Domains_Lattice T) st ( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds a [= b ) ) X c= the carrier of (Open_Domains_Lattice T) ; then A1: X c= Open_Domains_of T by Th103; then reconsider F = X as Subset-Family of T by TOPS_2:2; set A = Int (Cl (union F)); A2: F is open-domains-family by A1, Th79; then Int (Cl (union F)) is open_condensed by Th83; then Int (Cl (union F)) in { C where C is Subset of T : C is open_condensed } ; then A3: Int (Cl (union F)) in Open_Domains_of T by TDLAT_1:def_9; then reconsider a = Int (Cl (union F)) as Element of (Open_Domains_Lattice T) by Th103; A4: for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds a [= b proof let b be Element of (Open_Domains_Lattice T); ::_thesis: ( X is_less_than b implies a [= b ) reconsider B = b as Element of Open_Domains_of T by Th103; assume A5: X is_less_than b ; ::_thesis: a [= b A6: for C being Subset of T st C in F holds C c= B proof let C be Subset of T; ::_thesis: ( C in F implies C c= B ) reconsider C1 = C as Subset of T ; assume A7: C in F ; ::_thesis: C c= B then C1 is open_condensed by A2, Def4; then C in { P where P is Subset of T : P is open_condensed } ; then A8: C in Open_Domains_of T by TDLAT_1:def_9; then reconsider c = C as Element of (Open_Domains_Lattice T) by Th103; c [= b by A5, A7, LATTICE3:def_17; hence C c= B by A8, Th106; ::_thesis: verum end; B in Open_Domains_of T ; then B in { C where C is Subset of T : C is open_condensed } by TDLAT_1:def_9; then ex C being Subset of T st ( C = B & C is open_condensed ) ; then Int (Cl (union F)) c= B by A6, Th84; hence a [= b by A3, Th106; ::_thesis: verum end; take a ; ::_thesis: ( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds a [= b ) ) X is_less_than a proof let b be Element of (Open_Domains_Lattice T); :: according to LATTICE3:def_17 ::_thesis: ( not b in X or b [= a ) reconsider B = b as Element of Open_Domains_of T by Th103; assume b in X ; ::_thesis: b [= a then B c= Int (Cl (union F)) by A2, Th81, Th84; hence b [= a by A3, Th106; ::_thesis: verum end; hence ( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds a [= b ) ) by A4; ::_thesis: verum end; theorem Th108: :: TDLAT_2:108 for T being non empty TopSpace holds Open_Domains_Lattice T is complete proof let T be non empty TopSpace; ::_thesis: Open_Domains_Lattice T is complete thus for X being set ex a being Element of (Open_Domains_Lattice T) st ( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds a [= b ) ) :: according to LATTICE3:def_18 ::_thesis: verum proof let X be set ; ::_thesis: ex a being Element of (Open_Domains_Lattice T) st ( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds a [= b ) ) set Y = { c where c is Element of (Open_Domains_Lattice T) : c in X } ; A1: for d being Element of (Open_Domains_Lattice T) st { c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d holds X is_less_than d proof let d be Element of (Open_Domains_Lattice T); ::_thesis: ( { c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d implies X is_less_than d ) assume A2: { c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d ; ::_thesis: X is_less_than d thus for e being Element of (Open_Domains_Lattice T) st e in X holds e [= d :: according to LATTICE3:def_17 ::_thesis: verum proof let e be Element of (Open_Domains_Lattice T); ::_thesis: ( e in X implies e [= d ) assume e in X ; ::_thesis: e [= d then e in { c where c is Element of (Open_Domains_Lattice T) : c in X } ; hence e [= d by A2, LATTICE3:def_17; ::_thesis: verum end; end; A3: for d being Element of (Open_Domains_Lattice T) st X is_less_than d holds { c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d proof let d be Element of (Open_Domains_Lattice T); ::_thesis: ( X is_less_than d implies { c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d ) assume A4: X is_less_than d ; ::_thesis: { c where c is Element of (Open_Domains_Lattice T) : c in X } is_less_than d thus for e being Element of (Open_Domains_Lattice T) st e in { c where c is Element of (Open_Domains_Lattice T) : c in X } holds e [= d :: according to LATTICE3:def_17 ::_thesis: verum proof let e be Element of (Open_Domains_Lattice T); ::_thesis: ( e in { c where c is Element of (Open_Domains_Lattice T) : c in X } implies e [= d ) assume e in { c where c is Element of (Open_Domains_Lattice T) : c in X } ; ::_thesis: e [= d then ex e0 being Element of (Open_Domains_Lattice T) st ( e0 = e & e0 in X ) ; hence e [= d by A4, LATTICE3:def_17; ::_thesis: verum end; end; now__::_thesis:_for_x_being_set_st_x_in__{__c_where_c_is_Element_of_(Open_Domains_Lattice_T)_:_c_in_X__}__holds_ x_in_the_carrier_of_(Open_Domains_Lattice_T) let x be set ; ::_thesis: ( x in { c where c is Element of (Open_Domains_Lattice T) : c in X } implies x in the carrier of (Open_Domains_Lattice T) ) assume x in { c where c is Element of (Open_Domains_Lattice T) : c in X } ; ::_thesis: x in the carrier of (Open_Domains_Lattice T) then ex y being Element of (Open_Domains_Lattice T) st ( y = x & y in X ) ; hence x in the carrier of (Open_Domains_Lattice T) ; ::_thesis: verum end; then reconsider Y = { c where c is Element of (Open_Domains_Lattice T) : c in X } as Subset of (Open_Domains_Lattice T) by TARSKI:def_3; consider a being Element of (Open_Domains_Lattice T) such that A5: Y is_less_than a and A6: for b being Element of (Open_Domains_Lattice T) st Y is_less_than b holds a [= b by Th107; take a ; ::_thesis: ( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds a [= b ) ) for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds a [= b by A3, A6; hence ( X is_less_than a & ( for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds a [= b ) ) by A1, A5; ::_thesis: verum end; end; theorem :: TDLAT_2:109 for T being non empty TopSpace for F being Subset-Family of T st F is open-domains-family holds for X being Subset of (Open_Domains_Lattice T) st X = F holds "\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F)) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is open-domains-family holds for X being Subset of (Open_Domains_Lattice T) st X = F holds "\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F)) let F be Subset-Family of T; ::_thesis: ( F is open-domains-family implies for X being Subset of (Open_Domains_Lattice T) st X = F holds "\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F)) ) assume A1: F is open-domains-family ; ::_thesis: for X being Subset of (Open_Domains_Lattice T) st X = F holds "\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F)) let X be Subset of (Open_Domains_Lattice T); ::_thesis: ( X = F implies "\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F)) ) assume A2: X = F ; ::_thesis: "\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F)) thus "\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F)) ::_thesis: verum proof set A = Int (Cl (union F)); Int (Cl (union F)) is open_condensed by A1, Th83; then Int (Cl (union F)) in { C where C is Subset of T : C is open_condensed } ; then A3: Int (Cl (union F)) in Open_Domains_of T by TDLAT_1:def_9; then reconsider a = Int (Cl (union F)) as Element of (Open_Domains_Lattice T) by Th103; A4: X is_less_than a proof let b be Element of (Open_Domains_Lattice T); :: according to LATTICE3:def_17 ::_thesis: ( not b in X or b [= a ) reconsider B = b as Element of Open_Domains_of T by Th103; assume b in X ; ::_thesis: b [= a then B c= Int (Cl (union F)) by A1, A2, Th81, Th84; hence b [= a by A3, Th106; ::_thesis: verum end; A5: for b being Element of (Open_Domains_Lattice T) st X is_less_than b holds a [= b proof let b be Element of (Open_Domains_Lattice T); ::_thesis: ( X is_less_than b implies a [= b ) reconsider B = b as Element of Open_Domains_of T by Th103; assume A6: X is_less_than b ; ::_thesis: a [= b A7: for C being Subset of T st C in F holds C c= B proof let C be Subset of T; ::_thesis: ( C in F implies C c= B ) reconsider C1 = C as Subset of T ; assume A8: C in F ; ::_thesis: C c= B then C1 is open_condensed by A1, Def4; then C in { P where P is Subset of T : P is open_condensed } ; then A9: C in Open_Domains_of T by TDLAT_1:def_9; then reconsider c = C as Element of (Open_Domains_Lattice T) by Th103; c [= b by A2, A6, A8, LATTICE3:def_17; hence C c= B by A9, Th106; ::_thesis: verum end; B in Open_Domains_of T ; then B in { C where C is Subset of T : C is open_condensed } by TDLAT_1:def_9; then ex C being Subset of T st ( C = B & C is open_condensed ) ; then Int (Cl (union F)) c= B by A7, Th84; hence a [= b by A3, Th106; ::_thesis: verum end; Open_Domains_Lattice T is complete by Th108; hence "\/" (X,(Open_Domains_Lattice T)) = Int (Cl (union F)) by A4, A5, LATTICE3:def_21; ::_thesis: verum end; end; theorem :: TDLAT_2:110 for T being non empty TopSpace for F being Subset-Family of T st F is open-domains-family holds for X being Subset of (Open_Domains_Lattice T) st X = F holds ( ( X <> {} implies "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) ) & ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) ) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is open-domains-family holds for X being Subset of (Open_Domains_Lattice T) st X = F holds ( ( X <> {} implies "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) ) & ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) ) let F be Subset-Family of T; ::_thesis: ( F is open-domains-family implies for X being Subset of (Open_Domains_Lattice T) st X = F holds ( ( X <> {} implies "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) ) & ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) ) ) assume A1: F is open-domains-family ; ::_thesis: for X being Subset of (Open_Domains_Lattice T) st X = F holds ( ( X <> {} implies "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) ) & ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) ) let X be Subset of (Open_Domains_Lattice T); ::_thesis: ( X = F implies ( ( X <> {} implies "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) ) & ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) ) ) assume A2: X = F ; ::_thesis: ( ( X <> {} implies "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) ) & ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) ) thus ( X <> {} implies "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) ) ::_thesis: ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) proof set A = Int (meet F); Int (meet F) is open_condensed by A1, Th83; then Int (meet F) in { C where C is Subset of T : C is open_condensed } ; then A3: Int (meet F) in Open_Domains_of T by TDLAT_1:def_9; then reconsider a = Int (meet F) as Element of (Open_Domains_Lattice T) by Th103; A4: a is_less_than X proof let b be Element of (Open_Domains_Lattice T); :: according to LATTICE3:def_16 ::_thesis: ( not b in X or a [= b ) reconsider B = b as Element of Open_Domains_of T by Th103; assume b in X ; ::_thesis: a [= b then Int (meet F) c= B by A2, Th85; hence a [= b by A3, Th106; ::_thesis: verum end; assume A5: X <> {} ; ::_thesis: "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) A6: for b being Element of (Open_Domains_Lattice T) st b is_less_than X holds b [= a proof let b be Element of (Open_Domains_Lattice T); ::_thesis: ( b is_less_than X implies b [= a ) reconsider B = b as Element of Open_Domains_of T by Th103; assume A7: b is_less_than X ; ::_thesis: b [= a A8: for C being Subset of T st C in F holds B c= C proof let C be Subset of T; ::_thesis: ( C in F implies B c= C ) reconsider C1 = C as Subset of T ; assume A9: C in F ; ::_thesis: B c= C then C1 is open_condensed by A1, Def4; then C in { P where P is Subset of T : P is open_condensed } ; then A10: C in Open_Domains_of T by TDLAT_1:def_9; then reconsider c = C as Element of (Open_Domains_Lattice T) by Th103; b [= c by A2, A7, A9, LATTICE3:def_16; hence B c= C by A10, Th106; ::_thesis: verum end; B in Open_Domains_of T ; then B in { C where C is Subset of T : C is open_condensed } by TDLAT_1:def_9; then ex C being Subset of T st ( C = B & C is open_condensed ) ; then B c= Int (meet F) by A2, A5, A8, Th85; hence b [= a by A3, Th106; ::_thesis: verum end; Open_Domains_Lattice T is complete by Th108; hence "/\" (X,(Open_Domains_Lattice T)) = Int (meet F) by A4, A6, LATTICE3:34; ::_thesis: verum end; thus ( X = {} implies "/\" (X,(Open_Domains_Lattice T)) = [#] T ) ::_thesis: verum proof set A = [#] T; [#] T is open_condensed by TDLAT_1:21; then [#] T in { C where C is Subset of T : C is open_condensed } ; then A11: [#] T in Open_Domains_of T by TDLAT_1:def_9; then reconsider a = [#] T as Element of (Open_Domains_Lattice T) by Th103; A12: for b being Element of (Open_Domains_Lattice T) st b is_less_than X holds b [= a proof let b be Element of (Open_Domains_Lattice T); ::_thesis: ( b is_less_than X implies b [= a ) reconsider B = b as Element of Open_Domains_of T by Th103; assume b is_less_than X ; ::_thesis: b [= a B c= [#] T ; hence b [= a by A11, Th106; ::_thesis: verum end; assume A13: X = {} ; ::_thesis: "/\" (X,(Open_Domains_Lattice T)) = [#] T A14: a is_less_than X proof let b be Element of (Open_Domains_Lattice T); :: according to LATTICE3:def_16 ::_thesis: ( not b in X or a [= b ) assume b in X ; ::_thesis: a [= b hence a [= b by A13; ::_thesis: verum end; Open_Domains_Lattice T is complete by Th108; hence "/\" (X,(Open_Domains_Lattice T)) = [#] T by A14, A12, LATTICE3:34; ::_thesis: verum end; end; theorem :: TDLAT_2:111 for T being non empty TopSpace for F being Subset-Family of T st F is open-domains-family holds for X being Subset of (Domains_Lattice T) st X = F holds "\/" (X,(Domains_Lattice T)) = Int (Cl (union F)) proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is open-domains-family holds for X being Subset of (Domains_Lattice T) st X = F holds "\/" (X,(Domains_Lattice T)) = Int (Cl (union F)) let F be Subset-Family of T; ::_thesis: ( F is open-domains-family implies for X being Subset of (Domains_Lattice T) st X = F holds "\/" (X,(Domains_Lattice T)) = Int (Cl (union F)) ) A1: Int (union F) c= Int (Cl (union F)) by PRE_TOPC:18, TOPS_1:19; assume A2: F is open-domains-family ; ::_thesis: for X being Subset of (Domains_Lattice T) st X = F holds "\/" (X,(Domains_Lattice T)) = Int (Cl (union F)) then union F is open by Th81, TOPS_2:19; then union F c= Int (Cl (union F)) by A1, TOPS_1:23; then A3: (union F) \/ (Int (Cl (union F))) = Int (Cl (union F)) by XBOOLE_1:12; let X be Subset of (Domains_Lattice T); ::_thesis: ( X = F implies "\/" (X,(Domains_Lattice T)) = Int (Cl (union F)) ) assume X = F ; ::_thesis: "\/" (X,(Domains_Lattice T)) = Int (Cl (union F)) hence "\/" (X,(Domains_Lattice T)) = Int (Cl (union F)) by A2, A3, Th80, Th92; ::_thesis: verum end;