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