:: TDLAT_3 semantic presentation begin theorem Th1: :: TDLAT_3:1 for X being TopSpace for C being Subset of X holds Cl C = (Int (C `)) ` proof let X be TopSpace; ::_thesis: for C being Subset of X holds Cl C = (Int (C `)) ` let C be Subset of X; ::_thesis: Cl C = (Int (C `)) ` thus Cl C = ((Cl ((C `) `)) `) ` .= (Int (C `)) ` by TOPS_1:def_1 ; ::_thesis: verum end; theorem Th2: :: TDLAT_3:2 for X being TopSpace for C being Subset of X holds Cl (C `) = (Int C) ` proof let X be TopSpace; ::_thesis: for C being Subset of X holds Cl (C `) = (Int C) ` let C be Subset of X; ::_thesis: Cl (C `) = (Int C) ` thus Cl (C `) = (Int ((C `) `)) ` by Th1 .= (Int C) ` ; ::_thesis: verum end; theorem Th3: :: TDLAT_3:3 for X being TopSpace for C being Subset of X holds Int (C `) = (Cl C) ` proof let X be TopSpace; ::_thesis: for C being Subset of X holds Int (C `) = (Cl C) ` let C be Subset of X; ::_thesis: Int (C `) = (Cl C) ` thus Int (C `) = (Cl ((C `) `)) ` by TOPS_1:def_1 .= (Cl C) ` ; ::_thesis: verum end; theorem :: TDLAT_3:4 for X being TopSpace for A, B being Subset of X st A \/ B = the carrier of X & A is closed holds A \/ (Int B) = the carrier of X proof let X be TopSpace; ::_thesis: for A, B being Subset of X st A \/ B = the carrier of X & A is closed holds A \/ (Int B) = the carrier of X let A, B be Subset of X; ::_thesis: ( A \/ B = the carrier of X & A is closed implies A \/ (Int B) = the carrier of X ) assume A \/ B = the carrier of X ; ::_thesis: ( not A is closed or A \/ (Int B) = the carrier of X ) then (A \/ B) ` = {} X by XBOOLE_1:37; then (A `) /\ (B `) = {} by XBOOLE_1:53; then A1: A ` misses B ` by XBOOLE_0:def_7; assume A is closed ; ::_thesis: A \/ (Int B) = the carrier of X then A ` misses Cl (B `) by A1, TSEP_1:36; then (A `) /\ (((Cl (B `)) `) `) = {} by XBOOLE_0:def_7; then (A `) /\ ((Int B) `) = {} by TOPS_1:def_1; then (A \/ (Int B)) ` = {} X by XBOOLE_1:53; then ((A \/ (Int B)) `) ` = [#] X ; hence A \/ (Int B) = the carrier of X ; ::_thesis: verum end; theorem Th5: :: TDLAT_3:5 for X being TopSpace for A being Subset of X holds ( ( A is open & A is closed ) iff Cl A = Int A ) proof let X be TopSpace; ::_thesis: for A being Subset of X holds ( ( A is open & A is closed ) iff Cl A = Int A ) let A be Subset of X; ::_thesis: ( ( A is open & A is closed ) iff Cl A = Int A ) thus ( A is open & A is closed implies Cl A = Int A ) ::_thesis: ( Cl A = Int A implies ( A is open & A is closed ) ) proof assume that A1: A is open and A2: A is closed ; ::_thesis: Cl A = Int A Int A = A by A1, TOPS_1:23; hence Cl A = Int A by A2, PRE_TOPC:22; ::_thesis: verum end; A3: Int A c= A by TOPS_1:16; A4: A c= Cl A by PRE_TOPC:18; assume Cl A = Int A ; ::_thesis: ( A is open & A is closed ) hence ( A is open & A is closed ) by A3, A4, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: TDLAT_3:6 for X being TopSpace for A being Subset of X st A is open & A is closed holds Int (Cl A) = Cl (Int A) proof let X be TopSpace; ::_thesis: for A being Subset of X st A is open & A is closed holds Int (Cl A) = Cl (Int A) let A be Subset of X; ::_thesis: ( A is open & A is closed implies Int (Cl A) = Cl (Int A) ) assume that A1: A is open and A2: A is closed ; ::_thesis: Int (Cl A) = Cl (Int A) A3: Cl A = A by A2, PRE_TOPC:22; Int A = A by A1, TOPS_1:23; hence Int (Cl A) = Cl (Int A) by A3; ::_thesis: verum end; theorem Th7: :: TDLAT_3:7 for X being TopSpace for A being Subset of X st A is condensed & Cl (Int A) c= Int (Cl A) holds ( A is open_condensed & A is closed_condensed ) proof let X be TopSpace; ::_thesis: for A being Subset of X st A is condensed & Cl (Int A) c= Int (Cl A) holds ( A is open_condensed & A is closed_condensed ) let A be Subset of X; ::_thesis: ( A is condensed & Cl (Int A) c= Int (Cl A) implies ( A is open_condensed & A is closed_condensed ) ) assume A1: A is condensed ; ::_thesis: ( not Cl (Int A) c= Int (Cl A) or ( A is open_condensed & A is closed_condensed ) ) then A2: Int (Cl A) c= A by TOPS_1:def_6; A3: A c= Cl (Int A) by A1, TOPS_1:def_6; assume A4: Cl (Int A) c= Int (Cl A) ; ::_thesis: ( A is open_condensed & A is closed_condensed ) then Cl (Int A) c= A by A2, XBOOLE_1:1; then A5: A = Cl (Int A) by A3, XBOOLE_0:def_10; A c= Int (Cl A) by A3, A4, XBOOLE_1:1; then A = Int (Cl A) by A2, XBOOLE_0:def_10; hence ( A is open_condensed & A is closed_condensed ) by A5, TOPS_1:def_7, TOPS_1:def_8; ::_thesis: verum end; theorem Th8: :: TDLAT_3:8 for X being TopSpace for A being Subset of X st A is condensed & Cl (Int A) c= Int (Cl A) holds ( A is open & A is closed ) proof let X be TopSpace; ::_thesis: for A being Subset of X st A is condensed & Cl (Int A) c= Int (Cl A) holds ( A is open & A is closed ) let A be Subset of X; ::_thesis: ( A is condensed & Cl (Int A) c= Int (Cl A) implies ( A is open & A is closed ) ) assume that A1: A is condensed and A2: Cl (Int A) c= Int (Cl A) ; ::_thesis: ( A is open & A is closed ) A3: A is closed_condensed by A1, A2, Th7; A is open_condensed by A1, A2, Th7; hence ( A is open & A is closed ) by A3, TOPS_1:66, TOPS_1:67; ::_thesis: verum end; theorem Th9: :: TDLAT_3:9 for X being TopSpace for A being Subset of X st A is condensed holds ( Int (Cl A) = Int A & Cl A = Cl (Int A) ) proof let X be TopSpace; ::_thesis: for A being Subset of X st A is condensed holds ( Int (Cl A) = Int A & Cl A = Cl (Int A) ) let A be Subset of X; ::_thesis: ( A is condensed implies ( Int (Cl A) = Int A & Cl A = Cl (Int A) ) ) A1: Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16; assume A2: A is condensed ; ::_thesis: ( Int (Cl A) = Int A & Cl A = Cl (Int A) ) then Int (Cl A) c= A by TOPS_1:def_6; then A3: Int (Int (Cl A)) c= Int A by TOPS_1:19; A c= Cl (Int A) by A2, TOPS_1:def_6; then A4: Cl A c= Cl (Cl (Int A)) by PRE_TOPC:19; Int A c= Int (Cl A) by PRE_TOPC:18, TOPS_1:19; hence ( Int (Cl A) = Int A & Cl A = Cl (Int A) ) by A3, A4, A1, XBOOLE_0:def_10; ::_thesis: verum end; begin definition let IT be TopStruct ; attrIT is discrete means :Def1: :: TDLAT_3:def 1 the topology of IT = bool the carrier of IT; attrIT is anti-discrete means :Def2: :: TDLAT_3:def 2 the topology of IT = {{}, the carrier of IT}; end; :: deftheorem Def1 defines discrete TDLAT_3:def_1_:_ for IT being TopStruct holds ( IT is discrete iff the topology of IT = bool the carrier of IT ); :: deftheorem Def2 defines anti-discrete TDLAT_3:def_2_:_ for IT being TopStruct holds ( IT is anti-discrete iff the topology of IT = {{}, the carrier of IT} ); theorem :: TDLAT_3:10 for Y being TopStruct st Y is discrete & Y is anti-discrete holds bool the carrier of Y = {{}, the carrier of Y} proof let Y be TopStruct ; ::_thesis: ( Y is discrete & Y is anti-discrete implies bool the carrier of Y = {{}, the carrier of Y} ) assume that A1: Y is discrete and A2: Y is anti-discrete ; ::_thesis: bool the carrier of Y = {{}, the carrier of Y} the topology of Y = bool the carrier of Y by A1, Def1; hence bool the carrier of Y = {{}, the carrier of Y} by A2, Def2; ::_thesis: verum end; theorem Th11: :: TDLAT_3:11 for Y being TopStruct st {} in the topology of Y & the carrier of Y in the topology of Y & bool the carrier of Y = {{}, the carrier of Y} holds ( Y is discrete & Y is anti-discrete ) proof let Y be TopStruct ; ::_thesis: ( {} in the topology of Y & the carrier of Y in the topology of Y & bool the carrier of Y = {{}, the carrier of Y} implies ( Y is discrete & Y is anti-discrete ) ) assume that A1: {} in the topology of Y and A2: the carrier of Y in the topology of Y ; ::_thesis: ( not bool the carrier of Y = {{}, the carrier of Y} or ( Y is discrete & Y is anti-discrete ) ) assume A3: bool the carrier of Y = {{}, the carrier of Y} ; ::_thesis: ( Y is discrete & Y is anti-discrete ) {{}, the carrier of Y} c= the topology of Y by A1, A2, ZFMISC_1:32; then the topology of Y = bool the carrier of Y by A3, XBOOLE_0:def_10; hence ( Y is discrete & Y is anti-discrete ) by A3, Def1, Def2; ::_thesis: verum end; registration cluster non empty strict discrete anti-discrete for TopStruct ; existence ex b1 being TopStruct st ( b1 is discrete & b1 is anti-discrete & b1 is strict & not b1 is empty ) proof set one = {{}}; reconsider tau = bool {{}} as Subset-Family of {{}} ; take Y = TopStruct(# {{}},tau #); ::_thesis: ( Y is discrete & Y is anti-discrete & Y is strict & not Y is empty ) thus Y is discrete by Def1; ::_thesis: ( Y is anti-discrete & Y is strict & not Y is empty ) tau = {{},{{}}} by ZFMISC_1:24; hence Y is anti-discrete by Def2; ::_thesis: ( Y is strict & not Y is empty ) thus ( Y is strict & not Y is empty ) ; ::_thesis: verum end; end; theorem Th12: :: TDLAT_3:12 for Y being discrete TopStruct for A being Subset of Y holds the carrier of Y \ A in the topology of Y proof let Y be discrete TopStruct ; ::_thesis: for A being Subset of Y holds the carrier of Y \ A in the topology of Y let A be Subset of Y; ::_thesis: the carrier of Y \ A in the topology of Y the topology of Y = bool the carrier of Y by Def1; hence the carrier of Y \ A in the topology of Y ; ::_thesis: verum end; theorem Th13: :: TDLAT_3:13 for Y being anti-discrete TopStruct for A being Subset of Y st A in the topology of Y holds the carrier of Y \ A in the topology of Y proof let Y be anti-discrete TopStruct ; ::_thesis: for A being Subset of Y st A in the topology of Y holds the carrier of Y \ A in the topology of Y let A be Subset of Y; ::_thesis: ( A in the topology of Y implies the carrier of Y \ A in the topology of Y ) A1: the topology of Y = {{}, the carrier of Y} by Def2; assume A in the topology of Y ; ::_thesis: the carrier of Y \ A in the topology of Y then ( A = {} or A = the carrier of Y ) by A1, TARSKI:def_2; then ( the carrier of Y \ A = the carrier of Y or the carrier of Y \ A = {} ) by XBOOLE_1:37; hence the carrier of Y \ A in the topology of Y by A1, TARSKI:def_2; ::_thesis: verum end; registration cluster discrete -> TopSpace-like for TopStruct ; coherence for b1 being TopStruct st b1 is discrete holds b1 is TopSpace-like proof let Y be TopStruct ; ::_thesis: ( Y is discrete implies Y is TopSpace-like ) assume Y is discrete ; ::_thesis: Y is TopSpace-like then A1: the topology of Y = bool the carrier of Y by Def1; then A2: for F being Subset-Family of Y st F c= the topology of Y holds union F in the topology of Y ; A3: for A, B being Subset of Y st A in the topology of Y & B in the topology of Y holds A /\ B in the topology of Y by A1; the carrier of Y in the topology of Y by A1, ZFMISC_1:def_1; hence Y is TopSpace-like by A2, A3, PRE_TOPC:def_1; ::_thesis: verum end; cluster anti-discrete -> TopSpace-like for TopStruct ; coherence for b1 being TopStruct st b1 is anti-discrete holds b1 is TopSpace-like proof let Y be TopStruct ; ::_thesis: ( Y is anti-discrete implies Y is TopSpace-like ) assume Y is anti-discrete ; ::_thesis: Y is TopSpace-like then A4: the topology of Y = {{}, the carrier of Y} by Def2; A5: for A, B being Subset of Y st A in the topology of Y & B in the topology of Y holds A /\ B in the topology of Y proof let A, B be Subset of Y; ::_thesis: ( A in the topology of Y & B in the topology of Y implies A /\ B in the topology of Y ) assume that A6: A in the topology of Y and A7: B in the topology of Y ; ::_thesis: A /\ B in the topology of Y A8: ( B = {} or B = the carrier of Y ) by A4, A7, TARSKI:def_2; ( A = {} or A = the carrier of Y ) by A4, A6, TARSKI:def_2; hence A /\ B in the topology of Y by A4, A8, TARSKI:def_2; ::_thesis: verum end; A9: for F being Subset-Family of Y st F c= the topology of Y holds union F in the topology of Y proof let F be Subset-Family of Y; ::_thesis: ( F c= the topology of Y implies union F in the topology of Y ) assume F c= the topology of Y ; ::_thesis: union F in the topology of Y then ( F = {} or F = {{}} or F = { the carrier of Y} or F = {{}, the carrier of Y} ) by A4, ZFMISC_1:36; then ( union F = {} or union F = the carrier of Y or union F = {} \/ the carrier of Y ) by ZFMISC_1:2, ZFMISC_1:25, ZFMISC_1:75; hence union F in the topology of Y by A4, TARSKI:def_2; ::_thesis: verum end; the carrier of Y in the topology of Y by A4, TARSKI:def_2; hence Y is TopSpace-like by A9, A5, PRE_TOPC:def_1; ::_thesis: verum end; end; theorem :: TDLAT_3:14 for Y being TopSpace-like TopStruct st bool the carrier of Y = {{}, the carrier of Y} holds ( Y is discrete & Y is anti-discrete ) proof let Y be TopSpace-like TopStruct ; ::_thesis: ( bool the carrier of Y = {{}, the carrier of Y} implies ( Y is discrete & Y is anti-discrete ) ) reconsider E = {} as Subset-Family of Y by XBOOLE_1:2; reconsider E = E as Subset-Family of Y ; A1: the carrier of Y in the topology of Y by PRE_TOPC:def_1; E c= the topology of Y by XBOOLE_1:2; then A2: {} in the topology of Y by PRE_TOPC:def_1, ZFMISC_1:2; assume bool the carrier of Y = {{}, the carrier of Y} ; ::_thesis: ( Y is discrete & Y is anti-discrete ) hence ( Y is discrete & Y is anti-discrete ) by A2, A1, Th11; ::_thesis: verum end; definition let IT be TopStruct ; attrIT is almost_discrete means :Def3: :: TDLAT_3:def 3 for A being Subset of IT st A in the topology of IT holds the carrier of IT \ A in the topology of IT; end; :: deftheorem Def3 defines almost_discrete TDLAT_3:def_3_:_ for IT being TopStruct holds ( IT is almost_discrete iff for A being Subset of IT st A in the topology of IT holds the carrier of IT \ A in the topology of IT ); registration cluster discrete -> almost_discrete for TopStruct ; coherence for b1 being TopStruct st b1 is discrete holds b1 is almost_discrete proof let Y be TopStruct ; ::_thesis: ( Y is discrete implies Y is almost_discrete ) assume Y is discrete ; ::_thesis: Y is almost_discrete then for A being Subset of Y st A in the topology of Y holds the carrier of Y \ A in the topology of Y by Th12; hence Y is almost_discrete by Def3; ::_thesis: verum end; cluster anti-discrete -> almost_discrete for TopStruct ; coherence for b1 being TopStruct st b1 is anti-discrete holds b1 is almost_discrete proof let Y be TopStruct ; ::_thesis: ( Y is anti-discrete implies Y is almost_discrete ) assume Y is anti-discrete ; ::_thesis: Y is almost_discrete then for A being Subset of Y st A in the topology of Y holds the carrier of Y \ A in the topology of Y by Th13; hence Y is almost_discrete by Def3; ::_thesis: verum end; end; registration cluster strict almost_discrete for TopStruct ; existence ex b1 being TopStruct st ( b1 is almost_discrete & b1 is strict ) proof set Y = the strict discrete TopStruct ; take the strict discrete TopStruct ; ::_thesis: ( the strict discrete TopStruct is almost_discrete & the strict discrete TopStruct is strict ) thus ( the strict discrete TopStruct is almost_discrete & the strict discrete TopStruct is strict ) ; ::_thesis: verum end; end; begin registration cluster non empty strict TopSpace-like discrete anti-discrete for TopStruct ; existence ex b1 being TopSpace st ( b1 is discrete & b1 is anti-discrete & b1 is strict & not b1 is empty ) proof set X = the non empty strict discrete anti-discrete TopStruct ; reconsider X = the non empty strict discrete anti-discrete TopStruct as TopSpace ; take X ; ::_thesis: ( X is discrete & X is anti-discrete & X is strict & not X is empty ) thus ( X is discrete & X is anti-discrete & X is strict & not X is empty ) ; ::_thesis: verum end; end; theorem Th15: :: TDLAT_3:15 for X being TopSpace holds ( X is discrete iff for A being Subset of X holds A is open ) proof let X be TopSpace; ::_thesis: ( X is discrete iff for A being Subset of X holds A is open ) thus ( X is discrete implies for A being Subset of X holds A is open ) ::_thesis: ( ( for A being Subset of X holds A is open ) implies X is discrete ) proof assume A1: X is discrete ; ::_thesis: for A being Subset of X holds A is open let A be Subset of X; ::_thesis: A is open the topology of X = bool the carrier of X by A1, Def1; hence A is open by PRE_TOPC:def_2; ::_thesis: verum end; assume A2: for A being Subset of X holds A is open ; ::_thesis: X is discrete for V being set holds ( V in the topology of X iff V in bool the carrier of X ) proof let V be set ; ::_thesis: ( V in the topology of X iff V in bool the carrier of X ) now__::_thesis:_(_V_in_bool_the_carrier_of_X_implies_V_in_the_topology_of_X_) assume V in bool the carrier of X ; ::_thesis: V in the topology of X then reconsider C = V as Subset of X ; C is open by A2; hence V in the topology of X by PRE_TOPC:def_2; ::_thesis: verum end; hence ( V in the topology of X iff V in bool the carrier of X ) ; ::_thesis: verum end; then the topology of X = bool the carrier of X by TARSKI:1; hence X is discrete by Def1; ::_thesis: verum end; theorem Th16: :: TDLAT_3:16 for X being TopSpace holds ( X is discrete iff for A being Subset of X holds A is closed ) proof let X be TopSpace; ::_thesis: ( X is discrete iff for A being Subset of X holds A is closed ) thus ( X is discrete implies for A being Subset of X holds A is closed ) ::_thesis: ( ( for A being Subset of X holds A is closed ) implies X is discrete ) proof assume A1: X is discrete ; ::_thesis: for A being Subset of X holds A is closed let A be Subset of X; ::_thesis: A is closed A ` is open by A1, Th15; hence A is closed by TOPS_1:3; ::_thesis: verum end; assume A2: for A being Subset of X holds A is closed ; ::_thesis: X is discrete now__::_thesis:_for_A_being_Subset_of_X_holds_A_is_open let A be Subset of X; ::_thesis: A is open A ` is closed by A2; hence A is open by TOPS_1:4; ::_thesis: verum end; hence X is discrete by Th15; ::_thesis: verum end; theorem Th17: :: TDLAT_3:17 for X being TopSpace st ( for A being Subset of X for x being Point of X st A = {x} holds A is open ) holds X is discrete proof let X be TopSpace; ::_thesis: ( ( for A being Subset of X for x being Point of X st A = {x} holds A is open ) implies X is discrete ) assume A1: for A being Subset of X for x being Point of X st A = {x} holds A is open ; ::_thesis: X is discrete now__::_thesis:_for_A_being_Subset_of_X_holds_A_is_open let A be Subset of X; ::_thesis: A is open set F = { B where B is Subset of X : ex a being Point of X st ( a in A & B = {a} ) } ; A2: { B where B is Subset of X : ex a being Point of X st ( a in A & B = {a} ) } c= bool A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { B where B is Subset of X : ex a being Point of X st ( a in A & B = {a} ) } or x in bool A ) assume x in { B where B is Subset of X : ex a being Point of X st ( a in A & B = {a} ) } ; ::_thesis: x in bool A then consider C being Subset of X such that A3: x = C and A4: ex a being Point of X st ( a in A & C = {a} ) ; C c= A by A4, ZFMISC_1:31; hence x in bool A by A3; ::_thesis: verum end; bool A c= bool the carrier of X by ZFMISC_1:67; then reconsider F = { B where B is Subset of X : ex a being Point of X st ( a in A & B = {a} ) } as Subset-Family of X by A2, XBOOLE_1:1; A5: union (bool A) = A by ZFMISC_1:81; now__::_thesis:_for_x_being_set_st_x_in_bool_A_holds_ x_c=_union_F let x be set ; ::_thesis: ( x in bool A implies x c= union F ) assume A6: x in bool A ; ::_thesis: x c= union F then reconsider P = x as Subset of X by XBOOLE_1:1; now__::_thesis:_for_y_being_set_st_y_in_P_holds_ y_in_union_F let y be set ; ::_thesis: ( y in P implies y in union F ) assume A7: y in P ; ::_thesis: y in union F then reconsider a = y as Point of X ; now__::_thesis:_ex_B0_being_set_st_ (_y_in_B0_&_B0_in_F_) take B0 = {a}; ::_thesis: ( y in B0 & B0 in F ) B0 is Subset of X by A7, ZFMISC_1:31; hence ( y in B0 & B0 in F ) by A6, A7, TARSKI:def_1; ::_thesis: verum end; hence y in union F by TARSKI:def_4; ::_thesis: verum end; hence x c= union F by TARSKI:def_3; ::_thesis: verum end; then A8: union (bool A) c= union F ; now__::_thesis:_for_B_being_Subset_of_X_st_B_in_F_holds_ B_is_open let B be Subset of X; ::_thesis: ( B in F implies B is open ) assume B in F ; ::_thesis: B is open then ex C being Subset of X st ( C = B & ex a being Point of X st ( a in A & C = {a} ) ) ; hence B is open by A1; ::_thesis: verum end; then A9: F is open by TOPS_2:def_1; union F c= union (bool A) by A2, ZFMISC_1:77; then union F = A by A8, A5, XBOOLE_0:def_10; hence A is open by A9, TOPS_2:19; ::_thesis: verum end; hence X is discrete by Th15; ::_thesis: verum end; registration let X be non empty discrete TopSpace; cluster -> closed open discrete for SubSpace of X; coherence for b1 being SubSpace of X holds ( b1 is open & b1 is closed & b1 is discrete ) proof let X0 be SubSpace of X; ::_thesis: ( X0 is open & X0 is closed & X0 is discrete ) thus X0 is open ::_thesis: ( X0 is closed & X0 is discrete ) proof let A be Subset of X; :: according to TSEP_1:def_1 ::_thesis: ( not A = the carrier of X0 or A is open ) thus ( not A = the carrier of X0 or A is open ) by Th15; ::_thesis: verum end; thus X0 is closed ::_thesis: X0 is discrete proof let A be Subset of X; :: according to BORSUK_1:def_11 ::_thesis: ( not A = the carrier of X0 or A is closed ) thus ( not A = the carrier of X0 or A is closed ) by Th16; ::_thesis: verum end; A1: the topology of X = bool the carrier of X by Def1; now__::_thesis:_for_S_being_set_st_S_in_bool_the_carrier_of_X0_holds_ S_in_the_topology_of_X0 let S be set ; ::_thesis: ( S in bool the carrier of X0 implies S in the topology of X0 ) assume S in bool the carrier of X0 ; ::_thesis: S in the topology of X0 then reconsider A = S as Subset of X0 ; the carrier of X0 c= the carrier of X by BORSUK_1:1; then reconsider B = A as Subset of X by XBOOLE_1:1; now__::_thesis:_ex_B_being_Subset_of_X_st_ (_B_in_the_topology_of_X_&_A_=_B_/\_([#]_X0)_) take B = B; ::_thesis: ( B in the topology of X & A = B /\ ([#] X0) ) thus ( B in the topology of X & A = B /\ ([#] X0) ) by A1, XBOOLE_1:28; ::_thesis: verum end; hence S in the topology of X0 by PRE_TOPC:def_4; ::_thesis: verum end; then bool the carrier of X0 c= the topology of X0 by TARSKI:def_3; hence the topology of X0 = bool the carrier of X0 by XBOOLE_0:def_10; :: according to TDLAT_3:def_1 ::_thesis: verum end; end; registration let X be non empty discrete TopSpace; cluster strict TopSpace-like closed open discrete almost_discrete for SubSpace of X; existence ex b1 being SubSpace of X st ( b1 is discrete & b1 is strict ) proof set X0 = the strict SubSpace of X; take the strict SubSpace of X ; ::_thesis: ( the strict SubSpace of X is discrete & the strict SubSpace of X is strict ) thus ( the strict SubSpace of X is discrete & the strict SubSpace of X is strict ) ; ::_thesis: verum end; end; theorem Th18: :: TDLAT_3:18 for X being TopSpace holds ( X is anti-discrete iff for A being Subset of X holds ( not A is open or A = {} or A = the carrier of X ) ) proof let X be TopSpace; ::_thesis: ( X is anti-discrete iff for A being Subset of X holds ( not A is open or A = {} or A = the carrier of X ) ) A1: the carrier of X in the topology of X by PRE_TOPC:def_1; thus ( X is anti-discrete implies for A being Subset of X holds ( not A is open or A = {} or A = the carrier of X ) ) ::_thesis: ( ( for A being Subset of X holds ( not A is open or A = {} or A = the carrier of X ) ) implies X is anti-discrete ) proof assume A2: X is anti-discrete ; ::_thesis: for A being Subset of X holds ( not A is open or A = {} or A = the carrier of X ) let A be Subset of X; ::_thesis: ( not A is open or A = {} or A = the carrier of X ) assume A is open ; ::_thesis: ( A = {} or A = the carrier of X ) then A in the topology of X by PRE_TOPC:def_2; then A in {{}, the carrier of X} by A2, Def2; hence ( A = {} or A = the carrier of X ) by TARSKI:def_2; ::_thesis: verum end; assume A3: for A being Subset of X holds ( not A is open or A = {} or A = the carrier of X ) ; ::_thesis: X is anti-discrete now__::_thesis:_for_P_being_set_st_P_in_the_topology_of_X_holds_ P_in_{{},_the_carrier_of_X} let P be set ; ::_thesis: ( P in the topology of X implies P in {{}, the carrier of X} ) assume A4: P in the topology of X ; ::_thesis: P in {{}, the carrier of X} then reconsider C = P as Subset of X ; C is open by A4, PRE_TOPC:def_2; then ( C = {} or C = the carrier of X ) by A3; hence P in {{}, the carrier of X} by TARSKI:def_2; ::_thesis: verum end; then A5: the topology of X c= {{}, the carrier of X} by TARSKI:def_3; {} in the topology of X by PRE_TOPC:1; then {{}, the carrier of X} c= the topology of X by A1, ZFMISC_1:32; then the topology of X = {{}, the carrier of X} by A5, XBOOLE_0:def_10; hence X is anti-discrete by Def2; ::_thesis: verum end; theorem Th19: :: TDLAT_3:19 for X being TopSpace holds ( X is anti-discrete iff for A being Subset of X holds ( not A is closed or A = {} or A = the carrier of X ) ) proof let X be TopSpace; ::_thesis: ( X is anti-discrete iff for A being Subset of X holds ( not A is closed or A = {} or A = the carrier of X ) ) thus ( X is anti-discrete implies for A being Subset of X holds ( not A is closed or A = {} or A = the carrier of X ) ) ::_thesis: ( ( for A being Subset of X holds ( not A is closed or A = {} or A = the carrier of X ) ) implies X is anti-discrete ) proof assume A1: X is anti-discrete ; ::_thesis: for A being Subset of X holds ( not A is closed or A = {} or A = the carrier of X ) let A be Subset of X; ::_thesis: ( not A is closed or A = {} or A = the carrier of X ) assume A is closed ; ::_thesis: ( A = {} or A = the carrier of X ) then ( A ` = {} or A ` = the carrier of X ) by A1, Th18; then ( (A `) ` = [#] X or (A `) ` = {} X ) by XBOOLE_1:37; hence ( A = {} or A = the carrier of X ) ; ::_thesis: verum end; assume A2: for A being Subset of X holds ( not A is closed or A = {} or A = the carrier of X ) ; ::_thesis: X is anti-discrete now__::_thesis:_for_B_being_Subset_of_X_holds_ (_not_B_is_open_or_B_=_{}_or_B_=_the_carrier_of_X_) let B be Subset of X; ::_thesis: ( not B is open or B = {} or B = the carrier of X ) assume B is open ; ::_thesis: ( B = {} or B = the carrier of X ) then ( B ` = {} or B ` = the carrier of X ) by A2; then ( (B `) ` = [#] X or (B `) ` = {} X ) by XBOOLE_1:37; hence ( B = {} or B = the carrier of X ) ; ::_thesis: verum end; hence X is anti-discrete by Th18; ::_thesis: verum end; theorem :: TDLAT_3:20 for X being TopSpace st ( for A being Subset of X for x being Point of X st A = {x} holds Cl A = the carrier of X ) holds X is anti-discrete proof let X be TopSpace; ::_thesis: ( ( for A being Subset of X for x being Point of X st A = {x} holds Cl A = the carrier of X ) implies X is anti-discrete ) assume A1: for A being Subset of X for x being Point of X st A = {x} holds Cl A = the carrier of X ; ::_thesis: X is anti-discrete for B being Subset of X holds ( not B is closed or B = {} or B = the carrier of X ) proof let B be Subset of X; ::_thesis: ( not B is closed or B = {} or B = the carrier of X ) assume A2: B is closed ; ::_thesis: ( B = {} or B = the carrier of X ) set z = the Element of B; assume A3: B <> {} ; ::_thesis: B = the carrier of X then reconsider x = the Element of B as Point of X by TARSKI:def_3; A4: {x} c= B by A3, ZFMISC_1:31; then reconsider A = {x} as Subset of X by XBOOLE_1:1; Cl A = the carrier of X by A1; then the carrier of X c= B by A2, A4, TOPS_1:5; hence B = the carrier of X by XBOOLE_0:def_10; ::_thesis: verum end; hence X is anti-discrete by Th19; ::_thesis: verum end; registration let X be non empty anti-discrete TopSpace; cluster -> anti-discrete for SubSpace of X; coherence for b1 being SubSpace of X holds b1 is anti-discrete proof let X0 be SubSpace of X; ::_thesis: X0 is anti-discrete A1: the topology of X = {{}, the carrier of X} by Def2; now__::_thesis:_for_S_being_set_st_S_in_the_topology_of_X0_holds_ S_in_{{},_the_carrier_of_X0} let S be set ; ::_thesis: ( S in the topology of X0 implies S in {{}, the carrier of X0} ) assume A2: S in the topology of X0 ; ::_thesis: S in {{}, the carrier of X0} then reconsider A = S as Subset of X0 ; consider B being Subset of X such that A3: B in the topology of X and A4: A = B /\ ([#] X0) by A2, PRE_TOPC:def_4; A5: ( B = the carrier of X implies A = the carrier of X0 ) by A4, BORSUK_1:1, XBOOLE_1:28; ( B = {} implies A = {} ) by A4; hence S in {{}, the carrier of X0} by A1, A3, A5, TARSKI:def_2; ::_thesis: verum end; then A6: the topology of X0 c= {{}, the carrier of X0} by TARSKI:def_3; now__::_thesis:_for_S_being_set_st_S_in_{{},_the_carrier_of_X0}_holds_ S_in_the_topology_of_X0 let S be set ; ::_thesis: ( S in {{}, the carrier of X0} implies S in the topology of X0 ) assume S in {{}, the carrier of X0} ; ::_thesis: S in the topology of X0 then ( S = {} or S = the carrier of X0 ) by TARSKI:def_2; hence S in the topology of X0 by PRE_TOPC:1, PRE_TOPC:def_1; ::_thesis: verum end; then {{}, the carrier of X0} c= the topology of X0 by TARSKI:def_3; then the topology of X0 = {{}, the carrier of X0} by A6, XBOOLE_0:def_10; hence X0 is anti-discrete by Def2; ::_thesis: verum end; end; registration let X be non empty anti-discrete TopSpace; cluster TopSpace-like anti-discrete almost_discrete for SubSpace of X; existence ex b1 being SubSpace of X st b1 is anti-discrete proof set X0 = the SubSpace of X; take the SubSpace of X ; ::_thesis: the SubSpace of X is anti-discrete thus the SubSpace of X is anti-discrete ; ::_thesis: verum end; end; theorem Th21: :: TDLAT_3:21 for X being TopSpace holds ( X is almost_discrete iff for A being Subset of X st A is open holds A is closed ) proof let X be TopSpace; ::_thesis: ( X is almost_discrete iff for A being Subset of X st A is open holds A is closed ) thus ( X is almost_discrete implies for A being Subset of X st A is open holds A is closed ) ::_thesis: ( ( for A being Subset of X st A is open holds A is closed ) implies X is almost_discrete ) proof assume A1: X is almost_discrete ; ::_thesis: for A being Subset of X st A is open holds A is closed now__::_thesis:_for_A_being_Subset_of_X_st_A_is_open_holds_ A_is_closed let A be Subset of X; ::_thesis: ( A is open implies A is closed ) assume A is open ; ::_thesis: A is closed then A in the topology of X by PRE_TOPC:def_2; then the carrier of X \ A in the topology of X by A1, Def3; then ([#] X) \ A is open by PRE_TOPC:def_2; hence A is closed by PRE_TOPC:def_3; ::_thesis: verum end; hence for A being Subset of X st A is open holds A is closed ; ::_thesis: verum end; assume A2: for A being Subset of X st A is open holds A is closed ; ::_thesis: X is almost_discrete now__::_thesis:_for_A_being_Subset_of_X_st_A_in_the_topology_of_X_holds_ the_carrier_of_X_\_A_in_the_topology_of_X let A be Subset of X; ::_thesis: ( A in the topology of X implies the carrier of X \ A in the topology of X ) reconsider A9 = A as Subset of X ; assume A in the topology of X ; ::_thesis: the carrier of X \ A in the topology of X then A9 is open by PRE_TOPC:def_2; then A9 is closed by A2; then ([#] X) \ A9 is open by PRE_TOPC:def_3; hence the carrier of X \ A in the topology of X by PRE_TOPC:def_2; ::_thesis: verum end; hence X is almost_discrete by Def3; ::_thesis: verum end; theorem Th22: :: TDLAT_3:22 for X being TopSpace holds ( X is almost_discrete iff for A being Subset of X st A is closed holds A is open ) proof let X be TopSpace; ::_thesis: ( X is almost_discrete iff for A being Subset of X st A is closed holds A is open ) thus ( X is almost_discrete implies for A being Subset of X st A is closed holds A is open ) ::_thesis: ( ( for A being Subset of X st A is closed holds A is open ) implies X is almost_discrete ) proof assume A1: X is almost_discrete ; ::_thesis: for A being Subset of X st A is closed holds A is open let A be Subset of X; ::_thesis: ( A is closed implies A is open ) assume A is closed ; ::_thesis: A is open then A ` is closed by A1, Th21; hence A is open by TOPS_1:4; ::_thesis: verum end; assume A2: for A being Subset of X st A is closed holds A is open ; ::_thesis: X is almost_discrete now__::_thesis:_for_A_being_Subset_of_X_st_A_is_open_holds_ A_is_closed let A be Subset of X; ::_thesis: ( A is open implies A is closed ) assume A is open ; ::_thesis: A is closed then A ` is open by A2; hence A is closed by TOPS_1:3; ::_thesis: verum end; hence X is almost_discrete by Th21; ::_thesis: verum end; theorem :: TDLAT_3:23 for X being TopSpace holds ( X is almost_discrete iff for A being Subset of X st A is open holds Cl A = A ) proof let X be TopSpace; ::_thesis: ( X is almost_discrete iff for A being Subset of X st A is open holds Cl A = A ) thus ( X is almost_discrete implies for A being Subset of X st A is open holds Cl A = A ) ::_thesis: ( ( for A being Subset of X st A is open holds Cl A = A ) implies X is almost_discrete ) proof assume A1: X is almost_discrete ; ::_thesis: for A being Subset of X st A is open holds Cl A = A let A be Subset of X; ::_thesis: ( A is open implies Cl A = A ) assume A is open ; ::_thesis: Cl A = A then A is closed by A1, Th21; hence Cl A = A by PRE_TOPC:22; ::_thesis: verum end; assume A2: for A being Subset of X st A is open holds Cl A = A ; ::_thesis: X is almost_discrete now__::_thesis:_for_A_being_Subset_of_X_st_A_is_open_holds_ A_is_closed let A be Subset of X; ::_thesis: ( A is open implies A is closed ) assume A is open ; ::_thesis: A is closed then Cl A = A by A2; hence A is closed ; ::_thesis: verum end; hence X is almost_discrete by Th21; ::_thesis: verum end; theorem :: TDLAT_3:24 for X being TopSpace holds ( X is almost_discrete iff for A being Subset of X st A is closed holds Int A = A ) proof let X be TopSpace; ::_thesis: ( X is almost_discrete iff for A being Subset of X st A is closed holds Int A = A ) thus ( X is almost_discrete implies for A being Subset of X st A is closed holds Int A = A ) ::_thesis: ( ( for A being Subset of X st A is closed holds Int A = A ) implies X is almost_discrete ) proof assume A1: X is almost_discrete ; ::_thesis: for A being Subset of X st A is closed holds Int A = A let A be Subset of X; ::_thesis: ( A is closed implies Int A = A ) assume A is closed ; ::_thesis: Int A = A then A is open by A1, Th22; hence Int A = A by TOPS_1:23; ::_thesis: verum end; assume A2: for A being Subset of X st A is closed holds Int A = A ; ::_thesis: X is almost_discrete now__::_thesis:_for_A_being_Subset_of_X_st_A_is_closed_holds_ A_is_open let A be Subset of X; ::_thesis: ( A is closed implies A is open ) assume A is closed ; ::_thesis: A is open then Int A = A by A2; hence A is open ; ::_thesis: verum end; hence X is almost_discrete by Th22; ::_thesis: verum end; registration cluster strict TopSpace-like almost_discrete for TopStruct ; existence ex b1 being TopSpace st ( b1 is almost_discrete & b1 is strict ) proof set X = the strict discrete TopSpace; take the strict discrete TopSpace ; ::_thesis: ( the strict discrete TopSpace is almost_discrete & the strict discrete TopSpace is strict ) thus ( the strict discrete TopSpace is almost_discrete & the strict discrete TopSpace is strict ) ; ::_thesis: verum end; end; theorem :: TDLAT_3:25 for X being TopSpace st ( for A being Subset of X for x being Point of X st A = {x} holds Cl A is open ) holds X is almost_discrete proof let X be TopSpace; ::_thesis: ( ( for A being Subset of X for x being Point of X st A = {x} holds Cl A is open ) implies X is almost_discrete ) assume A1: for D being Subset of X for x being Point of X st D = {x} holds Cl D is open ; ::_thesis: X is almost_discrete for A being Subset of X st A is closed holds A is open proof let A be Subset of X; ::_thesis: ( A is closed implies A is open ) set F = { B where B is Subset of X : ex C being Subset of X ex a being Point of X st ( a in A & C = {a} & B = Cl C ) } ; A2: union (bool A) = A by ZFMISC_1:81; assume A3: A is closed ; ::_thesis: A is open A4: for C being Subset of X for a being Point of X st a in A & C = {a} holds Cl C c= A proof let C be Subset of X; ::_thesis: for a being Point of X st a in A & C = {a} holds Cl C c= A let a be Point of X; ::_thesis: ( a in A & C = {a} implies Cl C c= A ) assume that A5: a in A and A6: C = {a} ; ::_thesis: Cl C c= A C c= A by A5, A6, ZFMISC_1:31; then Cl C c= Cl A by PRE_TOPC:19; hence Cl C c= A by A3, PRE_TOPC:22; ::_thesis: verum end; A7: { B where B is Subset of X : ex C being Subset of X ex a being Point of X st ( a in A & C = {a} & B = Cl C ) } c= bool A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { B where B is Subset of X : ex C being Subset of X ex a being Point of X st ( a in A & C = {a} & B = Cl C ) } or x in bool A ) assume x in { B where B is Subset of X : ex C being Subset of X ex a being Point of X st ( a in A & C = {a} & B = Cl C ) } ; ::_thesis: x in bool A then consider P being Subset of X such that A8: x = P and A9: ex C being Subset of X ex a being Point of X st ( a in A & C = {a} & P = Cl C ) ; P c= A by A4, A9; hence x in bool A by A8; ::_thesis: verum end; bool A c= bool the carrier of X by ZFMISC_1:67; then reconsider F = { B where B is Subset of X : ex C being Subset of X ex a being Point of X st ( a in A & C = {a} & B = Cl C ) } as Subset-Family of X by A7, XBOOLE_1:1; now__::_thesis:_for_x_being_set_st_x_in_bool_A_holds_ x_c=_union_F let x be set ; ::_thesis: ( x in bool A implies x c= union F ) assume A10: x in bool A ; ::_thesis: x c= union F then reconsider P = x as Subset of X by XBOOLE_1:1; now__::_thesis:_for_y_being_set_st_y_in_P_holds_ y_in_union_F let y be set ; ::_thesis: ( y in P implies y in union F ) assume A11: y in P ; ::_thesis: y in union F then reconsider a = y as Point of X ; now__::_thesis:_ex_B_being_Element_of_K10(_the_carrier_of_X)_st_ (_y_in_B_&_B_in_F_) reconsider P0 = {a} as Subset of X by A11, ZFMISC_1:31; take B = Cl P0; ::_thesis: ( y in B & B in F ) A12: P0 c= B by PRE_TOPC:18; a in P0 by TARSKI:def_1; hence ( y in B & B in F ) by A10, A11, A12; ::_thesis: verum end; hence y in union F by TARSKI:def_4; ::_thesis: verum end; hence x c= union F by TARSKI:def_3; ::_thesis: verum end; then A13: union (bool A) c= union F ; now__::_thesis:_for_D_being_Subset_of_X_st_D_in_F_holds_ D_is_open let D be Subset of X; ::_thesis: ( D in F implies D is open ) assume D in F ; ::_thesis: D is open then ex S being Subset of X st ( S = D & ex C being Subset of X ex a being Point of X st ( a in A & C = {a} & S = Cl C ) ) ; hence D is open by A1; ::_thesis: verum end; then A14: F is open by TOPS_2:def_1; union F c= union (bool A) by A7, ZFMISC_1:77; then union F = A by A13, A2, XBOOLE_0:def_10; hence A is open by A14, TOPS_2:19; ::_thesis: verum end; hence X is almost_discrete by Th22; ::_thesis: verum end; theorem :: TDLAT_3:26 for X being TopSpace holds ( X is discrete iff ( X is almost_discrete & ( for A being Subset of X for x being Point of X st A = {x} holds A is closed ) ) ) proof let X be TopSpace; ::_thesis: ( X is discrete iff ( X is almost_discrete & ( for A being Subset of X for x being Point of X st A = {x} holds A is closed ) ) ) thus ( X is discrete implies ( X is almost_discrete & ( for A being Subset of X for x being Point of X st A = {x} holds A is closed ) ) ) by Th16; ::_thesis: ( X is almost_discrete & ( for A being Subset of X for x being Point of X st A = {x} holds A is closed ) implies X is discrete ) assume A1: X is almost_discrete ; ::_thesis: ( ex A being Subset of X ex x being Point of X st ( A = {x} & not A is closed ) or X is discrete ) assume A2: for A being Subset of X for x being Point of X st A = {x} holds A is closed ; ::_thesis: X is discrete for A being Subset of X for x being Point of X st A = {x} holds A is open proof let A be Subset of X; ::_thesis: for x being Point of X st A = {x} holds A is open let x be Point of X; ::_thesis: ( A = {x} implies A is open ) assume A = {x} ; ::_thesis: A is open then A is closed by A2; hence A is open by A1, Th22; ::_thesis: verum end; hence X is discrete by Th17; ::_thesis: verum end; registration cluster TopSpace-like discrete -> almost_discrete for TopStruct ; coherence for b1 being TopSpace st b1 is discrete holds b1 is almost_discrete ; cluster TopSpace-like anti-discrete -> almost_discrete for TopStruct ; coherence for b1 being TopSpace st b1 is anti-discrete holds b1 is almost_discrete ; end; registration let X be non empty almost_discrete TopSpace; cluster non empty -> non empty almost_discrete for SubSpace of X; coherence for b1 being non empty SubSpace of X holds b1 is almost_discrete proof let X0 be non empty SubSpace of X; ::_thesis: X0 is almost_discrete now__::_thesis:_for_A0_being_Subset_of_X0_st_A0_is_open_holds_ A0_is_closed let A0 be Subset of X0; ::_thesis: ( A0 is open implies A0 is closed ) assume A0 is open ; ::_thesis: A0 is closed then consider A being Subset of X such that A1: A is open and A2: A0 = A /\ ([#] X0) by TOPS_2:24; A is closed by A1, Th21; hence A0 is closed by A2, PRE_TOPC:13; ::_thesis: verum end; hence X0 is almost_discrete by Th21; ::_thesis: verum end; end; registration let X be non empty almost_discrete TopSpace; cluster open -> closed for SubSpace of X; coherence for b1 being SubSpace of X st b1 is open holds b1 is closed proof let X0 be SubSpace of X; ::_thesis: ( X0 is open implies X0 is closed ) assume A1: X0 is open ; ::_thesis: X0 is closed let A be Subset of X; :: according to BORSUK_1:def_11 ::_thesis: ( not A = the carrier of X0 or A is closed ) assume A = the carrier of X0 ; ::_thesis: A is closed then A is open by A1, TSEP_1:def_1; hence A is closed by Th21; ::_thesis: verum end; cluster closed -> open for SubSpace of X; coherence for b1 being SubSpace of X st b1 is closed holds b1 is open proof let X0 be SubSpace of X; ::_thesis: ( X0 is closed implies X0 is open ) assume A2: X0 is closed ; ::_thesis: X0 is open let A be Subset of X; :: according to TSEP_1:def_1 ::_thesis: ( not A = the carrier of X0 or A is open ) assume A = the carrier of X0 ; ::_thesis: A is open then A is closed by A2, BORSUK_1:def_11; hence A is open by Th22; ::_thesis: verum end; end; registration let X be non empty almost_discrete TopSpace; cluster non empty strict TopSpace-like almost_discrete for SubSpace of X; existence ex b1 being SubSpace of X st ( b1 is almost_discrete & b1 is strict & not b1 is empty ) proof set X0 = the non empty strict SubSpace of X; take the non empty strict SubSpace of X ; ::_thesis: ( the non empty strict SubSpace of X is almost_discrete & the non empty strict SubSpace of X is strict & not the non empty strict SubSpace of X is empty ) thus ( the non empty strict SubSpace of X is almost_discrete & the non empty strict SubSpace of X is strict & not the non empty strict SubSpace of X is empty ) ; ::_thesis: verum end; end; begin definition let IT be non empty TopSpace; attrIT is extremally_disconnected means :Def4: :: TDLAT_3:def 4 for A being Subset of IT st A is open holds Cl A is open ; end; :: deftheorem Def4 defines extremally_disconnected TDLAT_3:def_4_:_ for IT being non empty TopSpace holds ( IT is extremally_disconnected iff for A being Subset of IT st A is open holds Cl A is open ); registration cluster non empty strict TopSpace-like extremally_disconnected for TopStruct ; existence ex b1 being non empty TopSpace st ( b1 is extremally_disconnected & b1 is strict ) proof set X = the non empty strict discrete TopSpace; take the non empty strict discrete TopSpace ; ::_thesis: ( the non empty strict discrete TopSpace is extremally_disconnected & the non empty strict discrete TopSpace is strict ) now__::_thesis:_for_A_being_Subset_of_the_non_empty_strict_discrete_TopSpace_st_A_is_open_holds_ Cl_A_is_open let A be Subset of the non empty strict discrete TopSpace; ::_thesis: ( A is open implies Cl A is open ) assume A1: A is open ; ::_thesis: Cl A is open A is closed by Th16; hence Cl A is open by A1, PRE_TOPC:22; ::_thesis: verum end; hence ( the non empty strict discrete TopSpace is extremally_disconnected & the non empty strict discrete TopSpace is strict ) by Def4; ::_thesis: verum end; end; theorem Th27: :: TDLAT_3:27 for X being non empty TopSpace holds ( X is extremally_disconnected iff for A being Subset of X st A is closed holds Int A is closed ) proof let X be non empty TopSpace; ::_thesis: ( X is extremally_disconnected iff for A being Subset of X st A is closed holds Int A is closed ) thus ( X is extremally_disconnected implies for A being Subset of X st A is closed holds Int A is closed ) ::_thesis: ( ( for A being Subset of X st A is closed holds Int A is closed ) implies X is extremally_disconnected ) proof assume A1: X is extremally_disconnected ; ::_thesis: for A being Subset of X st A is closed holds Int A is closed let A be Subset of X; ::_thesis: ( A is closed implies Int A is closed ) assume A is closed ; ::_thesis: Int A is closed then Cl (A `) is open by A1, Def4; then (Cl (A `)) ` is closed ; hence Int A is closed by TOPS_1:def_1; ::_thesis: verum end; assume A2: for A being Subset of X st A is closed holds Int A is closed ; ::_thesis: X is extremally_disconnected now__::_thesis:_for_A_being_Subset_of_X_st_A_is_open_holds_ Cl_A_is_open let A be Subset of X; ::_thesis: ( A is open implies Cl A is open ) assume A is open ; ::_thesis: Cl A is open then Int (A `) is closed by A2; then (Int (A `)) ` is open ; hence Cl A is open by Th1; ::_thesis: verum end; hence X is extremally_disconnected by Def4; ::_thesis: verum end; theorem Th28: :: TDLAT_3:28 for X being non empty TopSpace holds ( X is extremally_disconnected iff for A, B being Subset of X st A is open & B is open & A misses B holds Cl A misses Cl B ) proof let X be non empty TopSpace; ::_thesis: ( X is extremally_disconnected iff for A, B being Subset of X st A is open & B is open & A misses B holds Cl A misses Cl B ) thus ( X is extremally_disconnected implies for A, B being Subset of X st A is open & B is open & A misses B holds Cl A misses Cl B ) ::_thesis: ( ( for A, B being Subset of X st A is open & B is open & A misses B holds Cl A misses Cl B ) implies X is extremally_disconnected ) proof assume A1: X is extremally_disconnected ; ::_thesis: for A, B being Subset of X st A is open & B is open & A misses B holds Cl A misses Cl B let A, B be Subset of X; ::_thesis: ( A is open & B is open & A misses B implies Cl A misses Cl B ) assume that A2: A is open and A3: B is open ; ::_thesis: ( not A misses B or Cl A misses Cl B ) assume A misses B ; ::_thesis: Cl A misses Cl B then A4: A misses Cl B by A2, TSEP_1:36; Cl B is open by A1, A3, Def4; hence Cl A misses Cl B by A4, TSEP_1:36; ::_thesis: verum end; assume A5: for A, B being Subset of X st A is open & B is open & A misses B holds Cl A misses Cl B ; ::_thesis: X is extremally_disconnected now__::_thesis:_for_A_being_Subset_of_X_st_A_is_open_holds_ Cl_A_is_open let A be Subset of X; ::_thesis: ( A is open implies Cl A is open ) A c= Cl A by PRE_TOPC:18; then A6: A misses (Cl A) ` by SUBSET_1:24; assume A is open ; ::_thesis: Cl A is open then Cl A misses Cl ((Cl A) `) by A5, A6; then Cl A c= (Cl ((Cl A) `)) ` by SUBSET_1:23; then A7: Cl A c= Int (Cl A) by TOPS_1:def_1; Int (Cl A) c= Cl A by TOPS_1:16; hence Cl A is open by A7, XBOOLE_0:def_10; ::_thesis: verum end; hence X is extremally_disconnected by Def4; ::_thesis: verum end; theorem :: TDLAT_3:29 for X being non empty TopSpace holds ( X is extremally_disconnected iff for A, B being Subset of X st A is closed & B is closed & A \/ B = the carrier of X holds (Int A) \/ (Int B) = the carrier of X ) proof let X be non empty TopSpace; ::_thesis: ( X is extremally_disconnected iff for A, B being Subset of X st A is closed & B is closed & A \/ B = the carrier of X holds (Int A) \/ (Int B) = the carrier of X ) thus ( X is extremally_disconnected implies for A, B being Subset of X st A is closed & B is closed & A \/ B = the carrier of X holds (Int A) \/ (Int B) = the carrier of X ) ::_thesis: ( ( for A, B being Subset of X st A is closed & B is closed & A \/ B = the carrier of X holds (Int A) \/ (Int B) = the carrier of X ) implies X is extremally_disconnected ) proof assume A1: X is extremally_disconnected ; ::_thesis: for A, B being Subset of X st A is closed & B is closed & A \/ B = the carrier of X holds (Int A) \/ (Int B) = the carrier of X let A, B be Subset of X; ::_thesis: ( A is closed & B is closed & A \/ B = the carrier of X implies (Int A) \/ (Int B) = the carrier of X ) assume that A2: A is closed and A3: B is closed ; ::_thesis: ( not A \/ B = the carrier of X or (Int A) \/ (Int B) = the carrier of X ) assume A \/ B = the carrier of X ; ::_thesis: (Int A) \/ (Int B) = the carrier of X then (A \/ B) ` = {} X by XBOOLE_1:37; then (A `) /\ (B `) = {} X by XBOOLE_1:53; then A ` misses B ` by XBOOLE_0:def_7; then Cl (A `) misses Cl (B `) by A1, A2, A3, Th28; then (Cl (A `)) /\ (Cl (B `)) = {} X by XBOOLE_0:def_7; then ((Cl (A `)) /\ (Cl (B `))) ` = [#] X ; then ((Cl (A `)) `) \/ ((Cl (B `)) `) = [#] X by XBOOLE_1:54; then ((Cl (A `)) `) \/ (Int B) = [#] X by TOPS_1:def_1; hence (Int A) \/ (Int B) = the carrier of X by TOPS_1:def_1; ::_thesis: verum end; assume A4: for A, B being Subset of X st A is closed & B is closed & A \/ B = the carrier of X holds (Int A) \/ (Int B) = the carrier of X ; ::_thesis: X is extremally_disconnected now__::_thesis:_for_A,_B_being_Subset_of_X_st_A_is_open_&_B_is_open_&_A_misses_B_holds_ Cl_A_misses_Cl_B let A, B be Subset of X; ::_thesis: ( A is open & B is open & A misses B implies Cl A misses Cl B ) assume that A5: A is open and A6: B is open ; ::_thesis: ( A misses B implies Cl A misses Cl B ) assume A misses B ; ::_thesis: Cl A misses Cl B then A /\ B = {} X by XBOOLE_0:def_7; then (A /\ B) ` = [#] X ; then (A `) \/ (B `) = [#] X by XBOOLE_1:54; then (Int (A `)) \/ (Int (B `)) = the carrier of X by A4, A5, A6; then ((Int (A `)) \/ (Int (B `))) ` = {} X by XBOOLE_1:37; then ((Int (A `)) `) /\ ((Int (B `)) `) = {} X by XBOOLE_1:53; then (Cl A) /\ ((Int (B `)) `) = {} X by Th1; then Cl A misses (Int (B `)) ` by XBOOLE_0:def_7; hence Cl A misses Cl B by Th1; ::_thesis: verum end; hence X is extremally_disconnected by Th28; ::_thesis: verum end; theorem Th30: :: TDLAT_3:30 for X being non empty TopSpace holds ( X is extremally_disconnected iff for A being Subset of X st A is open holds Cl A = Int (Cl A) ) proof let X be non empty TopSpace; ::_thesis: ( X is extremally_disconnected iff for A being Subset of X st A is open holds Cl A = Int (Cl A) ) thus ( X is extremally_disconnected implies for A being Subset of X st A is open holds Cl A = Int (Cl A) ) ::_thesis: ( ( for A being Subset of X st A is open holds Cl A = Int (Cl A) ) implies X is extremally_disconnected ) proof assume A1: X is extremally_disconnected ; ::_thesis: for A being Subset of X st A is open holds Cl A = Int (Cl A) let A be Subset of X; ::_thesis: ( A is open implies Cl A = Int (Cl A) ) A c= Cl A by PRE_TOPC:18; then A2: A misses (Cl A) ` by SUBSET_1:24; assume A is open ; ::_thesis: Cl A = Int (Cl A) then Cl A misses Cl ((Cl A) `) by A1, A2, Th28; then Cl A c= (Cl ((Cl A) `)) ` by SUBSET_1:23; then A3: Cl A c= Int (Cl A) by TOPS_1:def_1; Int (Cl A) c= Cl A by TOPS_1:16; hence Cl A = Int (Cl A) by A3, XBOOLE_0:def_10; ::_thesis: verum end; assume A4: for A being Subset of X st A is open holds Cl A = Int (Cl A) ; ::_thesis: X is extremally_disconnected now__::_thesis:_for_A_being_Subset_of_X_st_A_is_open_holds_ Cl_A_is_open let A be Subset of X; ::_thesis: ( A is open implies Cl A is open ) assume A is open ; ::_thesis: Cl A is open then Cl A = Int (Cl A) by A4; hence Cl A is open ; ::_thesis: verum end; hence X is extremally_disconnected by Def4; ::_thesis: verum end; theorem :: TDLAT_3:31 for X being non empty TopSpace holds ( X is extremally_disconnected iff for A being Subset of X st A is closed holds Int A = Cl (Int A) ) proof let X be non empty TopSpace; ::_thesis: ( X is extremally_disconnected iff for A being Subset of X st A is closed holds Int A = Cl (Int A) ) thus ( X is extremally_disconnected implies for A being Subset of X st A is closed holds Int A = Cl (Int A) ) ::_thesis: ( ( for A being Subset of X st A is closed holds Int A = Cl (Int A) ) implies X is extremally_disconnected ) proof assume A1: X is extremally_disconnected ; ::_thesis: for A being Subset of X st A is closed holds Int A = Cl (Int A) let A be Subset of X; ::_thesis: ( A is closed implies Int A = Cl (Int A) ) assume A is closed ; ::_thesis: Int A = Cl (Int A) then Cl (A `) = Int (Cl (A `)) by A1, Th30; then Int A = (Int (((Cl (A `)) `) `)) ` by TOPS_1:def_1; then Int A = Cl ((Cl (A `)) `) by Th1; hence Int A = Cl (Int A) ; ::_thesis: verum end; assume A2: for A being Subset of X st A is closed holds Int A = Cl (Int A) ; ::_thesis: X is extremally_disconnected now__::_thesis:_for_A_being_Subset_of_X_st_A_is_closed_holds_ Int_A_is_closed let A be Subset of X; ::_thesis: ( A is closed implies Int A is closed ) assume A is closed ; ::_thesis: Int A is closed then Int A = Cl (Int A) by A2; hence Int A is closed ; ::_thesis: verum end; hence X is extremally_disconnected by Th27; ::_thesis: verum end; theorem Th32: :: TDLAT_3:32 for X being non empty TopSpace holds ( X is extremally_disconnected iff for A being Subset of X st A is condensed holds ( A is closed & A is open ) ) proof let X be non empty TopSpace; ::_thesis: ( X is extremally_disconnected iff for A being Subset of X st A is condensed holds ( A is closed & A is open ) ) thus ( X is extremally_disconnected implies for A being Subset of X st A is condensed holds ( A is closed & A is open ) ) ::_thesis: ( ( for A being Subset of X st A is condensed holds ( A is closed & A is open ) ) implies X is extremally_disconnected ) proof assume A1: X is extremally_disconnected ; ::_thesis: for A being Subset of X st A is condensed holds ( A is closed & A is open ) let A be Subset of X; ::_thesis: ( A is condensed implies ( A is closed & A is open ) ) A2: Cl (Int A) is open by A1, Def4; assume A3: A is condensed ; ::_thesis: ( A is closed & A is open ) then Cl A = Cl (Int A) by Th9; then Int (Cl A) = Cl (Int A) by A2, TOPS_1:23; hence ( A is closed & A is open ) by A3, Th8; ::_thesis: verum end; assume A4: for A being Subset of X st A is condensed holds ( A is closed & A is open ) ; ::_thesis: X is extremally_disconnected now__::_thesis:_for_A_being_Subset_of_X_st_A_is_open_holds_ Cl_A_is_open let A be Subset of X; ::_thesis: ( A is open implies Cl A is open ) assume A is open ; ::_thesis: Cl A is open then A5: Int A = A by TOPS_1:23; Cl (Int A) is closed_condensed by TDLAT_1:22; then Cl A is condensed by A5, TOPS_1:66; hence Cl A is open by A4; ::_thesis: verum end; hence X is extremally_disconnected by Def4; ::_thesis: verum end; theorem Th33: :: TDLAT_3:33 for X being non empty TopSpace holds ( X is extremally_disconnected iff for A being Subset of X st A is condensed holds ( A is closed_condensed & A is open_condensed ) ) proof let X be non empty TopSpace; ::_thesis: ( X is extremally_disconnected iff for A being Subset of X st A is condensed holds ( A is closed_condensed & A is open_condensed ) ) thus ( X is extremally_disconnected implies for A being Subset of X st A is condensed holds ( A is closed_condensed & A is open_condensed ) ) ::_thesis: ( ( for A being Subset of X st A is condensed holds ( A is closed_condensed & A is open_condensed ) ) implies X is extremally_disconnected ) proof assume A1: X is extremally_disconnected ; ::_thesis: for A being Subset of X st A is condensed holds ( A is closed_condensed & A is open_condensed ) let A be Subset of X; ::_thesis: ( A is condensed implies ( A is closed_condensed & A is open_condensed ) ) assume A2: A is condensed ; ::_thesis: ( A is closed_condensed & A is open_condensed ) then A3: A is open by A1, Th32; A is closed by A1, A2, Th32; hence ( A is closed_condensed & A is open_condensed ) by A2, A3, TOPS_1:66, TOPS_1:67; ::_thesis: verum end; assume A4: for A being Subset of X st A is condensed holds ( A is closed_condensed & A is open_condensed ) ; ::_thesis: X is extremally_disconnected now__::_thesis:_for_A_being_Subset_of_X_st_A_is_condensed_holds_ (_A_is_closed_&_A_is_open_) let A be Subset of X; ::_thesis: ( A is condensed implies ( A is closed & A is open ) ) assume A5: A is condensed ; ::_thesis: ( A is closed & A is open ) then A6: A is open_condensed by A4; A is closed_condensed by A4, A5; hence ( A is closed & A is open ) by A6, TOPS_1:66, TOPS_1:67; ::_thesis: verum end; hence X is extremally_disconnected by Th32; ::_thesis: verum end; theorem Th34: :: TDLAT_3:34 for X being non empty TopSpace holds ( X is extremally_disconnected iff for A being Subset of X st A is condensed holds Int (Cl A) = Cl (Int A) ) proof let X be non empty TopSpace; ::_thesis: ( X is extremally_disconnected iff for A being Subset of X st A is condensed holds Int (Cl A) = Cl (Int A) ) thus ( X is extremally_disconnected implies for A being Subset of X st A is condensed holds Int (Cl A) = Cl (Int A) ) ::_thesis: ( ( for A being Subset of X st A is condensed holds Int (Cl A) = Cl (Int A) ) implies X is extremally_disconnected ) proof assume A1: X is extremally_disconnected ; ::_thesis: for A being Subset of X st A is condensed holds Int (Cl A) = Cl (Int A) let A be Subset of X; ::_thesis: ( A is condensed implies Int (Cl A) = Cl (Int A) ) assume A is condensed ; ::_thesis: Int (Cl A) = Cl (Int A) then A2: Cl A = Cl (Int A) by Th9; Cl (Int A) is open by A1, Def4; hence Int (Cl A) = Cl (Int A) by A2, TOPS_1:23; ::_thesis: verum end; assume A3: for A being Subset of X st A is condensed holds Int (Cl A) = Cl (Int A) ; ::_thesis: X is extremally_disconnected now__::_thesis:_for_A_being_Subset_of_X_st_A_is_condensed_holds_ (_A_is_closed_&_A_is_open_) let A be Subset of X; ::_thesis: ( A is condensed implies ( A is closed & A is open ) ) assume A4: A is condensed ; ::_thesis: ( A is closed & A is open ) then Int (Cl A) = Cl (Int A) by A3; hence ( A is closed & A is open ) by A4, Th8; ::_thesis: verum end; hence X is extremally_disconnected by Th32; ::_thesis: verum end; theorem :: TDLAT_3:35 for X being non empty TopSpace holds ( X is extremally_disconnected iff for A being Subset of X st A is condensed holds Int A = Cl A ) proof let X be non empty TopSpace; ::_thesis: ( X is extremally_disconnected iff for A being Subset of X st A is condensed holds Int A = Cl A ) thus ( X is extremally_disconnected implies for A being Subset of X st A is condensed holds Int A = Cl A ) ::_thesis: ( ( for A being Subset of X st A is condensed holds Int A = Cl A ) implies X is extremally_disconnected ) proof assume A1: X is extremally_disconnected ; ::_thesis: for A being Subset of X st A is condensed holds Int A = Cl A let A be Subset of X; ::_thesis: ( A is condensed implies Int A = Cl A ) assume A2: A is condensed ; ::_thesis: Int A = Cl A then A is closed by A1, Th32; then A3: A = Cl A by PRE_TOPC:22; A is open by A1, A2, Th32; hence Int A = Cl A by A3, TOPS_1:23; ::_thesis: verum end; assume A4: for A being Subset of X st A is condensed holds Int A = Cl A ; ::_thesis: X is extremally_disconnected now__::_thesis:_for_A_being_Subset_of_X_st_A_is_condensed_holds_ (_A_is_closed_&_A_is_open_) let A be Subset of X; ::_thesis: ( A is condensed implies ( A is closed & A is open ) ) assume A is condensed ; ::_thesis: ( A is closed & A is open ) then Int A = Cl A by A4; hence ( A is closed & A is open ) by Th5; ::_thesis: verum end; hence X is extremally_disconnected by Th32; ::_thesis: verum end; theorem Th36: :: TDLAT_3:36 for X being non empty TopSpace holds ( X is extremally_disconnected iff for A being Subset of X holds ( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) ) proof let X be non empty TopSpace; ::_thesis: ( X is extremally_disconnected iff for A being Subset of X holds ( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) ) thus ( X is extremally_disconnected implies for A being Subset of X holds ( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) ) ::_thesis: ( ( for A being Subset of X holds ( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) ) implies X is extremally_disconnected ) proof assume A1: X is extremally_disconnected ; ::_thesis: for A being Subset of X holds ( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) let A be Subset of X; ::_thesis: ( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) thus ( A is open_condensed implies A is closed_condensed ) ::_thesis: ( A is closed_condensed implies A is open_condensed ) proof assume A is open_condensed ; ::_thesis: A is closed_condensed then A is condensed by TOPS_1:67; hence A is closed_condensed by A1, Th33; ::_thesis: verum end; thus ( A is closed_condensed implies A is open_condensed ) ::_thesis: verum proof assume A is closed_condensed ; ::_thesis: A is open_condensed then A is condensed by TOPS_1:66; hence A is open_condensed by A1, Th33; ::_thesis: verum end; end; assume A2: for A being Subset of X holds ( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) ; ::_thesis: X is extremally_disconnected for A being Subset of X st A is condensed holds Int (Cl A) = Cl (Int A) proof let A be Subset of X; ::_thesis: ( A is condensed implies Int (Cl A) = Cl (Int A) ) assume A3: A is condensed ; ::_thesis: Int (Cl A) = Cl (Int A) then A4: A c= Cl (Int A) by TOPS_1:def_6; Cl (Int A) is closed_condensed by TDLAT_1:22; then Cl (Int A) is open_condensed by A2; then Cl (Int A) = Int (Cl (Cl (Int A))) by TOPS_1:def_8; then A5: Cl (Int A) c= Int (Cl A) by TDLAT_2:1; Int (Cl A) c= A by A3, TOPS_1:def_6; then Int (Cl A) c= Cl (Int A) by A4, XBOOLE_1:1; hence Int (Cl A) = Cl (Int A) by A5, XBOOLE_0:def_10; ::_thesis: verum end; hence X is extremally_disconnected by Th34; ::_thesis: verum end; definition let IT be non empty TopSpace; attrIT is hereditarily_extremally_disconnected means :Def5: :: TDLAT_3:def 5 for X0 being non empty SubSpace of IT holds X0 is extremally_disconnected ; end; :: deftheorem Def5 defines hereditarily_extremally_disconnected TDLAT_3:def_5_:_ for IT being non empty TopSpace holds ( IT is hereditarily_extremally_disconnected iff for X0 being non empty SubSpace of IT holds X0 is extremally_disconnected ); registration cluster non empty strict TopSpace-like hereditarily_extremally_disconnected for TopStruct ; existence ex b1 being non empty TopSpace st ( b1 is hereditarily_extremally_disconnected & b1 is strict ) proof set X = the non empty strict discrete TopSpace; take the non empty strict discrete TopSpace ; ::_thesis: ( the non empty strict discrete TopSpace is hereditarily_extremally_disconnected & the non empty strict discrete TopSpace is strict ) now__::_thesis:_for_X0_being_non_empty_SubSpace_of_the_non_empty_strict_discrete_TopSpace_holds_X0_is_extremally_disconnected let X0 be non empty SubSpace of the non empty strict discrete TopSpace; ::_thesis: X0 is extremally_disconnected now__::_thesis:_for_A_being_Subset_of_X0_st_A_is_open_holds_ Cl_A_is_open let A be Subset of X0; ::_thesis: ( A is open implies Cl A is open ) assume A1: A is open ; ::_thesis: Cl A is open A is closed by Th16; hence Cl A is open by A1, PRE_TOPC:22; ::_thesis: verum end; hence X0 is extremally_disconnected by Def4; ::_thesis: verum end; hence ( the non empty strict discrete TopSpace is hereditarily_extremally_disconnected & the non empty strict discrete TopSpace is strict ) by Def5; ::_thesis: verum end; end; registration cluster non empty TopSpace-like hereditarily_extremally_disconnected -> non empty extremally_disconnected for TopStruct ; coherence for b1 being non empty TopSpace st b1 is hereditarily_extremally_disconnected holds b1 is extremally_disconnected proof let X be non empty TopSpace; ::_thesis: ( X is hereditarily_extremally_disconnected implies X is extremally_disconnected ) assume A1: X is hereditarily_extremally_disconnected ; ::_thesis: X is extremally_disconnected X is SubSpace of X by TSEP_1:2; hence X is extremally_disconnected by A1, Def5; ::_thesis: verum end; cluster non empty TopSpace-like almost_discrete -> non empty hereditarily_extremally_disconnected for TopStruct ; coherence for b1 being non empty TopSpace st b1 is almost_discrete holds b1 is hereditarily_extremally_disconnected proof let X be non empty TopSpace; ::_thesis: ( X is almost_discrete implies X is hereditarily_extremally_disconnected ) assume X is almost_discrete ; ::_thesis: X is hereditarily_extremally_disconnected then reconsider X = X as non empty almost_discrete TopSpace ; now__::_thesis:_for_X0_being_non_empty_SubSpace_of_X_holds_X0_is_extremally_disconnected let X0 be non empty SubSpace of X; ::_thesis: X0 is extremally_disconnected now__::_thesis:_for_A_being_Subset_of_X0_st_A_is_open_holds_ Cl_A_is_open let A be Subset of X0; ::_thesis: ( A is open implies Cl A is open ) assume A2: A is open ; ::_thesis: Cl A is open then A is closed by Th21; hence Cl A is open by A2, PRE_TOPC:22; ::_thesis: verum end; hence X0 is extremally_disconnected by Def4; ::_thesis: verum end; hence X is hereditarily_extremally_disconnected by Def5; ::_thesis: verum end; end; theorem Th37: :: TDLAT_3:37 for X being non empty extremally_disconnected TopSpace for X0 being non empty SubSpace of X for A being Subset of X st A = the carrier of X0 & A is dense holds X0 is extremally_disconnected proof let X be non empty extremally_disconnected TopSpace; ::_thesis: for X0 being non empty SubSpace of X for A being Subset of X st A = the carrier of X0 & A is dense holds X0 is extremally_disconnected let X0 be non empty SubSpace of X; ::_thesis: for A being Subset of X st A = the carrier of X0 & A is dense holds X0 is extremally_disconnected let A be Subset of X; ::_thesis: ( A = the carrier of X0 & A is dense implies X0 is extremally_disconnected ) assume A1: A = the carrier of X0 ; ::_thesis: ( not A is dense or X0 is extremally_disconnected ) assume A2: A is dense ; ::_thesis: X0 is extremally_disconnected for D0, B0 being Subset of X0 st D0 is open & B0 is open & D0 misses B0 holds Cl D0 misses Cl B0 proof let D0, B0 be Subset of X0; ::_thesis: ( D0 is open & B0 is open & D0 misses B0 implies Cl D0 misses Cl B0 ) assume that A3: D0 is open and A4: B0 is open ; ::_thesis: ( not D0 misses B0 or Cl D0 misses Cl B0 ) consider D being Subset of X such that A5: D is open and A6: D /\ ([#] X0) = D0 by A3, TOPS_2:24; consider B being Subset of X such that A7: B is open and A8: B /\ ([#] X0) = B0 by A4, TOPS_2:24; assume A9: D0 /\ B0 = {} ; :: according to XBOOLE_0:def_7 ::_thesis: Cl D0 misses Cl B0 D misses B proof assume D /\ B <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then D /\ B meets A by A2, A5, A7, TOPS_1:45; then (D /\ B) /\ A <> {} by XBOOLE_0:def_7; then D /\ (B /\ (A /\ A)) <> {} by XBOOLE_1:16; then D /\ (A /\ (B /\ A)) <> {} by XBOOLE_1:16; hence contradiction by A1, A6, A8, A9, XBOOLE_1:16; ::_thesis: verum end; then Cl D misses Cl B by A5, A7, Th28; then (Cl D) /\ (Cl B) = {} by XBOOLE_0:def_7; then ((Cl D) /\ (Cl B)) /\ ([#] X0) = {} ; then (Cl D) /\ ((Cl B) /\ (([#] X0) /\ ([#] X0))) = {} by XBOOLE_1:16; then (Cl D) /\ (([#] X0) /\ ((Cl B) /\ ([#] X0))) = {} by XBOOLE_1:16; then A10: ((Cl D) /\ ([#] X0)) /\ ((Cl B) /\ ([#] X0)) = {} by XBOOLE_1:16; A11: Cl B0 c= (Cl B) /\ ([#] X0) proof B0 c= B by A8, XBOOLE_1:17; then reconsider B1 = B0 as Subset of X by XBOOLE_1:1; Cl B1 c= Cl B by A8, PRE_TOPC:19, XBOOLE_1:17; then (Cl B1) /\ ([#] X0) c= (Cl B) /\ ([#] X0) by XBOOLE_1:26; hence Cl B0 c= (Cl B) /\ ([#] X0) by PRE_TOPC:17; ::_thesis: verum end; Cl D0 c= (Cl D) /\ ([#] X0) proof D0 c= D by A6, XBOOLE_1:17; then reconsider D1 = D0 as Subset of X by XBOOLE_1:1; Cl D1 c= Cl D by A6, PRE_TOPC:19, XBOOLE_1:17; then (Cl D1) /\ ([#] X0) c= (Cl D) /\ ([#] X0) by XBOOLE_1:26; hence Cl D0 c= (Cl D) /\ ([#] X0) by PRE_TOPC:17; ::_thesis: verum end; then (Cl D0) /\ (Cl B0) c= ((Cl D) /\ ([#] X0)) /\ ((Cl B) /\ ([#] X0)) by A11, XBOOLE_1:27; then (Cl D0) /\ (Cl B0) = {} by A10; hence Cl D0 misses Cl B0 by XBOOLE_0:def_7; ::_thesis: verum end; hence X0 is extremally_disconnected by Th28; ::_thesis: verum end; registration let X be non empty extremally_disconnected TopSpace; cluster non empty open -> non empty extremally_disconnected for SubSpace of X; coherence for b1 being non empty SubSpace of X st b1 is open holds b1 is extremally_disconnected proof let X0 be non empty SubSpace of X; ::_thesis: ( X0 is open implies X0 is extremally_disconnected ) assume A1: X0 is open ; ::_thesis: X0 is extremally_disconnected reconsider B = the carrier of X0 as Subset of X by TSEP_1:1; now__::_thesis:_for_A0_being_Subset_of_X0_st_A0_is_open_holds_ Cl_A0_is_open let A0 be Subset of X0; ::_thesis: ( A0 is open implies Cl A0 is open ) A0 c= B ; then reconsider A = A0 as Subset of X by XBOOLE_1:1; assume A0 is open ; ::_thesis: Cl A0 is open then A is open by A1, TSEP_1:17; then A2: Cl A is open by Def4; Cl A0 = (Cl A) /\ ([#] X0) by PRE_TOPC:17; hence Cl A0 is open by A2, TOPS_2:24; ::_thesis: verum end; hence X0 is extremally_disconnected by Def4; ::_thesis: verum end; end; registration let X be non empty extremally_disconnected TopSpace; cluster non empty strict TopSpace-like extremally_disconnected for SubSpace of X; existence ex b1 being non empty SubSpace of X st ( b1 is extremally_disconnected & b1 is strict ) proof set X0 = the non empty strict open SubSpace of X; take the non empty strict open SubSpace of X ; ::_thesis: ( the non empty strict open SubSpace of X is extremally_disconnected & the non empty strict open SubSpace of X is strict ) thus ( the non empty strict open SubSpace of X is extremally_disconnected & the non empty strict open SubSpace of X is strict ) ; ::_thesis: verum end; end; registration let X be non empty hereditarily_extremally_disconnected TopSpace; cluster non empty -> non empty hereditarily_extremally_disconnected for SubSpace of X; coherence for b1 being non empty SubSpace of X holds b1 is hereditarily_extremally_disconnected proof let X0 be non empty SubSpace of X; ::_thesis: X0 is hereditarily_extremally_disconnected for Y being non empty SubSpace of X0 holds Y is extremally_disconnected proof let Y be non empty SubSpace of X0; ::_thesis: Y is extremally_disconnected Y is SubSpace of X by TSEP_1:7; hence Y is extremally_disconnected by Def5; ::_thesis: verum end; hence X0 is hereditarily_extremally_disconnected by Def5; ::_thesis: verum end; end; registration let X be non empty hereditarily_extremally_disconnected TopSpace; cluster non empty strict TopSpace-like extremally_disconnected hereditarily_extremally_disconnected for SubSpace of X; existence ex b1 being non empty SubSpace of X st ( b1 is hereditarily_extremally_disconnected & b1 is strict ) proof set X0 = the non empty strict SubSpace of X; take the non empty strict SubSpace of X ; ::_thesis: ( the non empty strict SubSpace of X is hereditarily_extremally_disconnected & the non empty strict SubSpace of X is strict ) thus ( the non empty strict SubSpace of X is hereditarily_extremally_disconnected & the non empty strict SubSpace of X is strict ) ; ::_thesis: verum end; end; theorem :: TDLAT_3:38 for X being non empty TopSpace st ( for X0 being non empty closed SubSpace of X holds X0 is extremally_disconnected ) holds X is hereditarily_extremally_disconnected proof let X be non empty TopSpace; ::_thesis: ( ( for X0 being non empty closed SubSpace of X holds X0 is extremally_disconnected ) implies X is hereditarily_extremally_disconnected ) assume A1: for Y being non empty closed SubSpace of X holds Y is extremally_disconnected ; ::_thesis: X is hereditarily_extremally_disconnected for X0 being non empty SubSpace of X holds X0 is extremally_disconnected proof let X0 be non empty SubSpace of X; ::_thesis: X0 is extremally_disconnected reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1; set A = Cl A0; not Cl A0 is empty by PCOMPS_1:2; then consider Y being non empty strict closed SubSpace of X such that A2: Cl A0 = the carrier of Y by TSEP_1:15; A0 c= Cl A0 by PRE_TOPC:18; then reconsider Y0 = X0 as non empty SubSpace of Y by A2, TSEP_1:4; reconsider B0 = the carrier of Y0 as Subset of Y by TSEP_1:1; Cl B0 = (Cl A0) /\ ([#] Y) by PRE_TOPC:17; then A3: B0 is dense by A2, TOPS_1:def_3; Y is extremally_disconnected by A1; hence X0 is extremally_disconnected by A3, Th37; ::_thesis: verum end; hence X is hereditarily_extremally_disconnected by Def5; ::_thesis: verum end; begin theorem Th39: :: TDLAT_3:39 for Y being non empty extremally_disconnected TopSpace holds Domains_of Y = Closed_Domains_of Y proof let Y be non empty extremally_disconnected TopSpace; ::_thesis: Domains_of Y = Closed_Domains_of Y now__::_thesis:_for_S_being_set_st_S_in_Domains_of_Y_holds_ S_in_Closed_Domains_of_Y let S be set ; ::_thesis: ( S in Domains_of Y implies S in Closed_Domains_of Y ) assume A1: S in Domains_of Y ; ::_thesis: S in Closed_Domains_of Y then reconsider A = S as Subset of Y ; A in { D where D is Subset of Y : D is condensed } by A1, TDLAT_1:def_1; then ex D being Subset of Y st ( D = A & D is condensed ) ; then A is closed_condensed by Th33; then A in { E where E is Subset of Y : E is closed_condensed } ; hence S in Closed_Domains_of Y by TDLAT_1:def_5; ::_thesis: verum end; then A2: Domains_of Y c= Closed_Domains_of Y by TARSKI:def_3; Closed_Domains_of Y c= Domains_of Y by TDLAT_1:31; hence Domains_of Y = Closed_Domains_of Y by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th40: :: TDLAT_3:40 for Y being non empty extremally_disconnected TopSpace holds ( D-Union Y = CLD-Union Y & D-Meet Y = CLD-Meet Y ) proof let Y be non empty extremally_disconnected TopSpace; ::_thesis: ( D-Union Y = CLD-Union Y & D-Meet Y = CLD-Meet Y ) A1: Domains_of Y = Closed_Domains_of Y by Th39; hence D-Union Y = (D-Union Y) || (Closed_Domains_of Y) by RELSET_1:19 .= CLD-Union Y by TDLAT_1:39 ; ::_thesis: D-Meet Y = CLD-Meet Y thus D-Meet Y = (D-Meet Y) || (Closed_Domains_of Y) by A1, RELSET_1:19 .= CLD-Meet Y by TDLAT_1:40 ; ::_thesis: verum end; theorem Th41: :: TDLAT_3:41 for Y being non empty extremally_disconnected TopSpace holds Domains_Lattice Y = Closed_Domains_Lattice Y proof let Y be non empty extremally_disconnected TopSpace; ::_thesis: Domains_Lattice Y = Closed_Domains_Lattice Y A1: D-Union Y = CLD-Union Y by Th40; A2: D-Meet Y = CLD-Meet Y by Th40; Domains_of Y = Closed_Domains_of Y by Th39; hence Domains_Lattice Y = LattStr(# (Closed_Domains_of Y),(CLD-Union Y),(CLD-Meet Y) #) by A1, A2, TDLAT_1:def_4 .= Closed_Domains_Lattice Y by TDLAT_1:def_8 ; ::_thesis: verum end; theorem Th42: :: TDLAT_3:42 for Y being non empty extremally_disconnected TopSpace holds Domains_of Y = Open_Domains_of Y proof let Y be non empty extremally_disconnected TopSpace; ::_thesis: Domains_of Y = Open_Domains_of Y now__::_thesis:_for_S_being_set_st_S_in_Domains_of_Y_holds_ S_in_Open_Domains_of_Y let S be set ; ::_thesis: ( S in Domains_of Y implies S in Open_Domains_of Y ) assume A1: S in Domains_of Y ; ::_thesis: S in Open_Domains_of Y then reconsider A = S as Subset of Y ; A in { D where D is Subset of Y : D is condensed } by A1, TDLAT_1:def_1; then ex D being Subset of Y st ( D = A & D is condensed ) ; then A is open_condensed by Th33; then A in { E where E is Subset of Y : E is open_condensed } ; hence S in Open_Domains_of Y by TDLAT_1:def_9; ::_thesis: verum end; then A2: Domains_of Y c= Open_Domains_of Y by TARSKI:def_3; Open_Domains_of Y c= Domains_of Y by TDLAT_1:35; hence Domains_of Y = Open_Domains_of Y by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th43: :: TDLAT_3:43 for Y being non empty extremally_disconnected TopSpace holds ( D-Union Y = OPD-Union Y & D-Meet Y = OPD-Meet Y ) proof let Y be non empty extremally_disconnected TopSpace; ::_thesis: ( D-Union Y = OPD-Union Y & D-Meet Y = OPD-Meet Y ) A1: Domains_of Y = Open_Domains_of Y by Th42; hence D-Union Y = (D-Union Y) || (Open_Domains_of Y) by RELSET_1:19 .= OPD-Union Y by TDLAT_1:42 ; ::_thesis: D-Meet Y = OPD-Meet Y thus D-Meet Y = (D-Meet Y) || (Open_Domains_of Y) by A1, RELSET_1:19 .= OPD-Meet Y by TDLAT_1:43 ; ::_thesis: verum end; theorem Th44: :: TDLAT_3:44 for Y being non empty extremally_disconnected TopSpace holds Domains_Lattice Y = Open_Domains_Lattice Y proof let Y be non empty extremally_disconnected TopSpace; ::_thesis: Domains_Lattice Y = Open_Domains_Lattice Y A1: D-Union Y = OPD-Union Y by Th43; A2: D-Meet Y = OPD-Meet Y by Th43; Domains_of Y = Open_Domains_of Y by Th42; hence Domains_Lattice Y = LattStr(# (Open_Domains_of Y),(OPD-Union Y),(OPD-Meet Y) #) by A1, A2, TDLAT_1:def_4 .= Open_Domains_Lattice Y by TDLAT_1:def_12 ; ::_thesis: verum end; theorem Th45: :: TDLAT_3:45 for Y being non empty extremally_disconnected TopSpace for A, B being Element of Domains_of Y holds ( (D-Union Y) . (A,B) = A \/ B & (D-Meet Y) . (A,B) = A /\ B ) proof let Y be non empty extremally_disconnected TopSpace; ::_thesis: for A, B being Element of Domains_of Y holds ( (D-Union Y) . (A,B) = A \/ B & (D-Meet Y) . (A,B) = A /\ B ) let A, B be Element of Domains_of Y; ::_thesis: ( (D-Union Y) . (A,B) = A \/ B & (D-Meet Y) . (A,B) = A /\ B ) reconsider A0 = A, B0 = B as Element of Closed_Domains_of Y by Th39; (D-Union Y) . (A,B) = (CLD-Union Y) . (A0,B0) by Th40; hence (D-Union Y) . (A,B) = A \/ B by TDLAT_1:def_6; ::_thesis: (D-Meet Y) . (A,B) = A /\ B reconsider A0 = A, B0 = B as Element of Open_Domains_of Y by Th42; (D-Meet Y) . (A,B) = (OPD-Meet Y) . (A0,B0) by Th43; hence (D-Meet Y) . (A,B) = A /\ B by TDLAT_1:def_11; ::_thesis: verum end; theorem :: TDLAT_3:46 for Y being non empty extremally_disconnected TopSpace for a, b being Element of (Domains_Lattice Y) for A, B being Element of Domains_of Y st a = A & b = B holds ( a "\/" b = A \/ B & a "/\" b = A /\ B ) proof let Y be non empty extremally_disconnected TopSpace; ::_thesis: for a, b being Element of (Domains_Lattice Y) for A, B being Element of Domains_of Y st a = A & b = B holds ( a "\/" b = A \/ B & a "/\" b = A /\ B ) let a, b be Element of (Domains_Lattice Y); ::_thesis: for A, B being Element of Domains_of Y st a = A & b = B holds ( a "\/" b = A \/ B & a "/\" b = A /\ B ) let A, B be Element of Domains_of Y; ::_thesis: ( a = A & b = B implies ( a "\/" b = A \/ B & a "/\" b = A /\ B ) ) assume that A1: a = A and A2: b = B ; ::_thesis: ( a "\/" b = A \/ B & a "/\" b = A /\ B ) A3: Domains_Lattice Y = LattStr(# (Domains_of Y),(D-Union Y),(D-Meet Y) #) by TDLAT_1:def_4; hence a "\/" b = (D-Union Y) . (A,B) by A1, A2, LATTICES:def_1 .= A \/ B by Th45 ; ::_thesis: a "/\" b = A /\ B thus a "/\" b = (D-Meet Y) . (A,B) by A3, A1, A2, LATTICES:def_2 .= A /\ B by Th45 ; ::_thesis: verum end; theorem :: TDLAT_3:47 for Y being non empty extremally_disconnected TopSpace for F being Subset-Family of Y st F is domains-family holds for S being Subset of (Domains_Lattice Y) st S = F holds "\/" (S,(Domains_Lattice Y)) = Cl (union F) proof let Y be non empty extremally_disconnected TopSpace; ::_thesis: for F being Subset-Family of Y st F is domains-family holds for S being Subset of (Domains_Lattice Y) st S = F holds "\/" (S,(Domains_Lattice Y)) = Cl (union F) let F be Subset-Family of Y; ::_thesis: ( F is domains-family implies for S being Subset of (Domains_Lattice Y) st S = F holds "\/" (S,(Domains_Lattice Y)) = Cl (union F) ) assume F is domains-family ; ::_thesis: for S being Subset of (Domains_Lattice Y) st S = F holds "\/" (S,(Domains_Lattice Y)) = Cl (union F) then F c= Domains_of Y by TDLAT_2:65; then F c= Closed_Domains_of Y by Th39; then A1: F is closed-domains-family by TDLAT_2:72; let S be Subset of (Domains_Lattice Y); ::_thesis: ( S = F implies "\/" (S,(Domains_Lattice Y)) = Cl (union F) ) reconsider P = S as Subset of (Closed_Domains_Lattice Y) by Th41; assume A2: S = F ; ::_thesis: "\/" (S,(Domains_Lattice Y)) = Cl (union F) thus "\/" (S,(Domains_Lattice Y)) = "\/" (P,(Closed_Domains_Lattice Y)) by Th41 .= Cl (union F) by A1, A2, TDLAT_2:100 ; ::_thesis: verum end; theorem :: TDLAT_3:48 for Y being non empty extremally_disconnected TopSpace for F being Subset-Family of Y st F is domains-family holds for S being Subset of (Domains_Lattice Y) st S = F holds ( ( S <> {} implies "/\" (S,(Domains_Lattice Y)) = Int (meet F) ) & ( S = {} implies "/\" (S,(Domains_Lattice Y)) = [#] Y ) ) proof let Y be non empty extremally_disconnected TopSpace; ::_thesis: for F being Subset-Family of Y st F is domains-family holds for S being Subset of (Domains_Lattice Y) st S = F holds ( ( S <> {} implies "/\" (S,(Domains_Lattice Y)) = Int (meet F) ) & ( S = {} implies "/\" (S,(Domains_Lattice Y)) = [#] Y ) ) let F be Subset-Family of Y; ::_thesis: ( F is domains-family implies for S being Subset of (Domains_Lattice Y) st S = F holds ( ( S <> {} implies "/\" (S,(Domains_Lattice Y)) = Int (meet F) ) & ( S = {} implies "/\" (S,(Domains_Lattice Y)) = [#] Y ) ) ) assume A1: F is domains-family ; ::_thesis: for S being Subset of (Domains_Lattice Y) st S = F holds ( ( S <> {} implies "/\" (S,(Domains_Lattice Y)) = Int (meet F) ) & ( S = {} implies "/\" (S,(Domains_Lattice Y)) = [#] Y ) ) then F c= Domains_of Y by TDLAT_2:65; then F c= Open_Domains_of Y by Th42; then A2: F is open-domains-family by TDLAT_2:79; let S be Subset of (Domains_Lattice Y); ::_thesis: ( S = F implies ( ( S <> {} implies "/\" (S,(Domains_Lattice Y)) = Int (meet F) ) & ( S = {} implies "/\" (S,(Domains_Lattice Y)) = [#] Y ) ) ) assume A3: S = F ; ::_thesis: ( ( S <> {} implies "/\" (S,(Domains_Lattice Y)) = Int (meet F) ) & ( S = {} implies "/\" (S,(Domains_Lattice Y)) = [#] Y ) ) Domains_Lattice Y = Open_Domains_Lattice Y by Th44; hence ( S <> {} implies "/\" (S,(Domains_Lattice Y)) = Int (meet F) ) by A2, A3, TDLAT_2:110; ::_thesis: ( S = {} implies "/\" (S,(Domains_Lattice Y)) = [#] Y ) assume S = {} ; ::_thesis: "/\" (S,(Domains_Lattice Y)) = [#] Y hence "/\" (S,(Domains_Lattice Y)) = [#] Y by A1, A3, TDLAT_2:93; ::_thesis: verum end; theorem Th49: :: TDLAT_3:49 for X being non empty TopSpace holds ( X is extremally_disconnected iff Domains_Lattice X is M_Lattice ) proof let X be non empty TopSpace; ::_thesis: ( X is extremally_disconnected iff Domains_Lattice X is M_Lattice ) thus ( X is extremally_disconnected implies Domains_Lattice X is M_Lattice ) ::_thesis: ( Domains_Lattice X is M_Lattice implies X is extremally_disconnected ) proof assume X is extremally_disconnected ; ::_thesis: Domains_Lattice X is M_Lattice then Domains_Lattice X = Open_Domains_Lattice X by Th44; hence Domains_Lattice X is M_Lattice ; ::_thesis: verum end; assume A1: Domains_Lattice X is M_Lattice ; ::_thesis: X is extremally_disconnected assume not X is extremally_disconnected ; ::_thesis: contradiction then consider D being Subset of X such that A2: D is condensed and A3: Int (Cl D) <> Cl (Int D) by Th34; set A = Int (Cl D); set C = Cl (Int D); set B = (Cl (Int D)) ` ; A4: D c= Cl (Int D) by A2, TOPS_1:def_6; Int (Cl D) c= D by A2, TOPS_1:def_6; then A5: Int (Cl D) c= Cl (Int D) by A4, XBOOLE_1:1; A6: Int (Cl D) is open_condensed by TDLAT_1:23; then A7: Int (Cl D) = Int (Cl (Int (Cl D))) by TOPS_1:def_8; (Cl (Int D)) ` misses Cl (Int D) by XBOOLE_1:79; then A8: ((Cl (Int D)) `) /\ (Cl (Int D)) = {} X by XBOOLE_0:def_7; A9: Cl (Int D) is closed_condensed by TDLAT_1:22; then A10: Cl (Int D) = Cl (Int (Cl (Int D))) by TOPS_1:def_7; Cl (Int D) is condensed by A9, TOPS_1:66; then A11: Cl (Int D) in { E where E is Subset of X : E is condensed } ; then A12: Cl (Int D) in Domains_of X by TDLAT_1:def_1; A13: Domains_Lattice X = LattStr(# (Domains_of X),(D-Union X),(D-Meet X) #) by TDLAT_1:def_4; then reconsider c = Cl (Int D) as Element of (Domains_Lattice X) by A11, TDLAT_1:def_1; Int (Cl D) is condensed by A6, TOPS_1:67; then A14: Int (Cl D) in { E where E is Subset of X : E is condensed } ; then reconsider a = Int (Cl D) as Element of (Domains_Lattice X) by A13, TDLAT_1:def_1; A15: (Cl (Int D)) ` = Int ((Int D) `) by Th3 .= Int (Cl (D `)) by Th2 ; ((Cl (Int D)) `) ` is closed_condensed by TDLAT_1:22; then (Cl (Int D)) ` is open_condensed by TOPS_1:61; then (Cl (Int D)) ` is condensed by TOPS_1:67; then (Cl (Int D)) ` in { E where E is Subset of X : E is condensed } ; then reconsider b = (Cl (Int D)) ` as Element of (Domains_Lattice X) by A13, TDLAT_1:def_1; A16: (Int (Cl D)) \/ ({} X) = Int (Cl D) ; Cl ((Int (Cl D)) \/ ((Cl (Int D)) `)) = (Cl (Int (Cl D))) \/ (Cl ((Cl (Int D)) `)) by PRE_TOPC:20 .= Cl (Int ((Cl D) \/ (Cl (D `)))) by A15, TDLAT_1:6 .= Cl (Int (Cl (D \/ (D `)))) by PRE_TOPC:20 .= Cl (Int (Cl ([#] X))) by PRE_TOPC:2 .= Cl (Int ([#] X)) by TOPS_1:2 .= Cl ([#] X) by TOPS_1:15 .= [#] X by TOPS_1:2 ; then a "\/" b = (Int ([#] X)) \/ ((Int (Cl D)) \/ ((Cl (Int D)) `)) by A13, TDLAT_2:87 .= ([#] X) \/ ((Int (Cl D)) \/ ((Cl (Int D)) `)) by TOPS_1:15 .= [#] X by XBOOLE_1:12 ; then A17: (a "\/" b) "/\" c = (Cl (Int (([#] X) /\ (Cl (Int D))))) /\ (([#] X) /\ (Cl (Int D))) by A13, TDLAT_2:87 .= (Cl (Int (Cl (Int D)))) /\ (([#] X) /\ (Cl (Int D))) by XBOOLE_1:28 .= (Cl (Int (Cl (Int D)))) /\ (Cl (Int D)) by XBOOLE_1:28 .= Cl (Int D) by A10 ; Int (Cl D) in Domains_of X by A14, TDLAT_1:def_1; then A18: a [= c by A12, A5, TDLAT_2:89; b "/\" c = (Cl (Int (((Cl (Int D)) `) /\ (Cl (Int D))))) /\ (((Cl (Int D)) `) /\ (Cl (Int D))) by A13, TDLAT_2:87 .= {} X by A8 ; then a "\/" (b "/\" c) = (Int (Cl (Int (Cl D)))) \/ (Int (Cl D)) by A13, A16, TDLAT_2:87 .= Int (Cl D) by A7 ; hence contradiction by A1, A3, A18, A17, LATTICES:def_12; ::_thesis: verum end; theorem :: TDLAT_3:50 for X being non empty TopSpace st Domains_Lattice X = Closed_Domains_Lattice X holds X is extremally_disconnected by Th49; theorem :: TDLAT_3:51 for X being non empty TopSpace st Domains_Lattice X = Open_Domains_Lattice X holds X is extremally_disconnected by Th49; theorem :: TDLAT_3:52 for X being non empty TopSpace holds X is extremally_disconnected proof let X be non empty TopSpace; ::_thesis: X is extremally_disconnected for A being Subset of X holds ( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) proof let A be Subset of X; ::_thesis: ( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) thus ( A is open_condensed implies A is closed_condensed ) ::_thesis: ( A is closed_condensed implies A is open_condensed ) proof assume A is open_condensed ; ::_thesis: A is closed_condensed then A in { E where E is Subset of X : E is open_condensed } ; then A in { E where E is Subset of X : E is closed_condensed } ; then ex D being Subset of X st ( D = A & D is closed_condensed ) ; hence A is closed_condensed ; ::_thesis: verum end; assume A is closed_condensed ; ::_thesis: A is open_condensed then A in { E where E is Subset of X : E is closed_condensed } ; then A in { E where E is Subset of X : E is open_condensed } ; then ex D being Subset of X st ( D = A & D is open_condensed ) ; hence A is open_condensed ; ::_thesis: verum end; hence X is extremally_disconnected by Th36; ::_thesis: verum end; theorem :: TDLAT_3:53 for X being non empty TopSpace holds ( X is extremally_disconnected iff Domains_Lattice X is B_Lattice ) proof let X be non empty TopSpace; ::_thesis: ( X is extremally_disconnected iff Domains_Lattice X is B_Lattice ) thus ( X is extremally_disconnected implies Domains_Lattice X is B_Lattice ) ::_thesis: ( Domains_Lattice X is B_Lattice implies X is extremally_disconnected ) proof assume X is extremally_disconnected ; ::_thesis: Domains_Lattice X is B_Lattice then Domains_Lattice X = Open_Domains_Lattice X by Th44; hence Domains_Lattice X is B_Lattice ; ::_thesis: verum end; assume Domains_Lattice X is B_Lattice ; ::_thesis: X is extremally_disconnected hence X is extremally_disconnected by Th49; ::_thesis: verum end;