:: TDLAT_3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: TDLAT_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: TDLAT_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being TopSpace
for C being Subset of X holds Cl C = (Int (C ` )) `
proof end;

theorem Th3: :: TDLAT_3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being TopSpace
for C being Subset of X holds Cl (C ` ) = (Int C) `
proof end;

theorem Th4: :: TDLAT_3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being TopSpace
for C being Subset of X holds Int (C ` ) = (Cl C) `
proof end;

theorem :: TDLAT_3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TDLAT_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being TopSpace
for A, B being Subset of X st A \/ B = the carrier of X holds
( ( A is closed implies A \/ (Int B) = the carrier of X ) & ( B is closed implies (Int A) \/ B = the carrier of X ) )
proof end;

theorem Th7: :: TDLAT_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being TopSpace
for A being Subset of X holds
( ( A is open & A is closed ) iff Cl A = Int A )
proof end;

theorem :: TDLAT_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th9: :: TDLAT_3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th10: :: TDLAT_3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th11: :: TDLAT_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let IT be TopStruct ;
attr IT is discrete means :Def1: :: TDLAT_3:def 1
the topology of IT = bool the carrier of IT;
attr IT 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:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being TopStruct st Y is discrete & Y is anti-discrete holds
bool the carrier of Y = {{} ,the carrier of Y}
proof end;

theorem Th13: :: TDLAT_3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

registration
cluster non empty strict discrete anti-discrete TopStruct ;
existence
ex b1 being TopStruct st
( b1 is discrete & b1 is anti-discrete & b1 is strict & not b1 is empty )
proof end;
end;

theorem Th14: :: TDLAT_3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being discrete TopStruct
for A being Subset of Y holds the carrier of Y \ A in the topology of Y
proof end;

theorem Th15: :: TDLAT_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

registration
cluster discrete -> TopSpace-like TopStruct ;
coherence
for b1 being TopStruct st b1 is discrete holds
b1 is TopSpace-like
proof end;
cluster anti-discrete -> TopSpace-like TopStruct ;
coherence
for b1 being TopStruct st b1 is anti-discrete holds
b1 is TopSpace-like
proof end;
end;

theorem :: TDLAT_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let IT be TopStruct ;
attr IT 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 TopStruct ;
coherence
for b1 being TopStruct st b1 is discrete holds
b1 is almost_discrete
proof end;
cluster anti-discrete -> almost_discrete TopStruct ;
coherence
for b1 being TopStruct st b1 is anti-discrete holds
b1 is almost_discrete
proof end;
end;

registration
cluster strict almost_discrete TopStruct ;
existence
ex b1 being TopStruct st
( b1 is almost_discrete & b1 is strict )
proof end;
end;

registration
cluster non empty strict discrete anti-discrete almost_discrete TopStruct ;
existence
ex b1 being TopSpace st
( b1 is discrete & b1 is anti-discrete & b1 is strict & not b1 is empty )
proof end;
end;

theorem Th17: :: TDLAT_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being TopSpace holds
( X is discrete iff for A being Subset of X holds A is open )
proof end;

theorem Th18: :: TDLAT_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being TopSpace holds
( X is discrete iff for A being Subset of X holds A is closed )
proof end;

theorem Th19: :: TDLAT_3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

registration
let X be non empty discrete TopSpace;
cluster -> TopSpace-like closed open discrete almost_discrete SubSpace of X;
coherence
for b1 being SubSpace of X holds
( b1 is open & b1 is closed & b1 is discrete )
proof end;
end;

registration
let X be non empty discrete TopSpace;
cluster strict TopSpace-like closed open discrete almost_discrete SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is discrete & b1 is strict )
proof end;
end;

theorem Th20: :: TDLAT_3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th21: :: TDLAT_3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TDLAT_3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

registration
let X be non empty anti-discrete TopSpace;
cluster -> TopSpace-like anti-discrete almost_discrete SubSpace of X;
coherence
for b1 being SubSpace of X holds b1 is anti-discrete
proof end;
end;

registration
let X be non empty anti-discrete TopSpace;
cluster TopSpace-like anti-discrete almost_discrete SubSpace of X;
existence
ex b1 being SubSpace of X st b1 is anti-discrete
proof end;
end;

theorem Th23: :: TDLAT_3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th24: :: TDLAT_3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TDLAT_3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TDLAT_3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

registration
cluster strict almost_discrete TopStruct ;
existence
ex b1 being TopSpace st
( b1 is almost_discrete & b1 is strict )
proof end;
end;

theorem :: TDLAT_3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TDLAT_3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

registration
cluster discrete -> almost_discrete TopStruct ;
coherence
for b1 being TopSpace st b1 is discrete holds
b1 is almost_discrete
proof end;
cluster anti-discrete -> almost_discrete TopStruct ;
coherence
for b1 being TopSpace st b1 is anti-discrete holds
b1 is almost_discrete
proof end;
end;

registration
let X be non empty almost_discrete TopSpace;
cluster non empty -> non empty almost_discrete SubSpace of X;
coherence
for b1 being non empty SubSpace of X holds b1 is almost_discrete
proof end;
end;

registration
let X be non empty almost_discrete TopSpace;
cluster open -> closed SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is open holds
b1 is closed
proof end;
cluster closed -> open SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is closed holds
b1 is open
proof end;
end;

registration
let X be non empty almost_discrete TopSpace;
cluster non empty strict almost_discrete SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is almost_discrete & b1 is strict & not b1 is empty )
proof end;
end;

definition
let IT be non empty TopSpace;
attr IT 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 extremally_disconnected TopStruct ;
existence
ex b1 being non empty TopSpace st
( b1 is extremally_disconnected & b1 is strict )
proof end;
end;

theorem Th29: :: TDLAT_3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th30: :: TDLAT_3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TDLAT_3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th32: :: TDLAT_3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TDLAT_3:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th34: :: TDLAT_3:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th35: :: TDLAT_3:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th36: :: TDLAT_3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TDLAT_3:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th38: :: TDLAT_3:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let IT be non empty TopSpace;
attr IT 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 hereditarily_extremally_disconnected TopStruct ;
existence
ex b1 being non empty TopSpace st
( b1 is hereditarily_extremally_disconnected & b1 is strict )
proof end;
end;

registration
cluster non empty hereditarily_extremally_disconnected -> non empty extremally_disconnected TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is hereditarily_extremally_disconnected holds
b1 is extremally_disconnected
proof end;
cluster non empty almost_discrete -> non empty hereditarily_extremally_disconnected TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is almost_discrete holds
b1 is hereditarily_extremally_disconnected
proof end;
end;

theorem Th39: :: TDLAT_3:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

registration
let X be non empty extremally_disconnected TopSpace;
cluster non empty open -> non empty extremally_disconnected SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is open holds
b1 is extremally_disconnected
proof end;
end;

registration
let X be non empty extremally_disconnected TopSpace;
cluster non empty strict extremally_disconnected SubSpace of X;
existence
ex b1 being non empty SubSpace of X st
( b1 is extremally_disconnected & b1 is strict )
proof end;
end;

registration
let X be non empty hereditarily_extremally_disconnected TopSpace;
cluster non empty -> non empty extremally_disconnected hereditarily_extremally_disconnected SubSpace of X;
coherence
for b1 being non empty SubSpace of X holds b1 is hereditarily_extremally_disconnected
proof end;
end;

registration
let X be non empty hereditarily_extremally_disconnected TopSpace;
cluster non empty strict extremally_disconnected hereditarily_extremally_disconnected SubSpace of X;
existence
ex b1 being non empty SubSpace of X st
( b1 is hereditarily_extremally_disconnected & b1 is strict )
proof end;
end;

theorem :: TDLAT_3:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th41: :: TDLAT_3:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty extremally_disconnected TopSpace holds Domains_of Y = Closed_Domains_of Y
proof end;

theorem Th42: :: TDLAT_3:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty extremally_disconnected TopSpace holds
( D-Union Y = CLD-Union Y & D-Meet Y = CLD-Meet Y )
proof end;

theorem Th43: :: TDLAT_3:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty extremally_disconnected TopSpace holds Domains_Lattice Y = Closed_Domains_Lattice Y
proof end;

theorem Th44: :: TDLAT_3:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty extremally_disconnected TopSpace holds Domains_of Y = Open_Domains_of Y
proof end;

theorem Th45: :: TDLAT_3:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty extremally_disconnected TopSpace holds
( D-Union Y = OPD-Union Y & D-Meet Y = OPD-Meet Y )
proof end;

theorem Th46: :: TDLAT_3:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty extremally_disconnected TopSpace holds Domains_Lattice Y = Open_Domains_Lattice Y
proof end;

theorem Th47: :: TDLAT_3:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TDLAT_3:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TDLAT_3:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TDLAT_3:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th51: :: TDLAT_3:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace holds
( X is extremally_disconnected iff Domains_Lattice X is M_Lattice )
proof end;

theorem :: TDLAT_3:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace st Domains_Lattice X = Closed_Domains_Lattice X holds
X is extremally_disconnected by Th51;

theorem :: TDLAT_3:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace st Domains_Lattice X = Open_Domains_Lattice X holds
X is extremally_disconnected by Th51;

theorem :: TDLAT_3:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace st Closed_Domains_Lattice X = Open_Domains_Lattice X holds
X is extremally_disconnected
proof end;

theorem :: TDLAT_3:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace holds
( X is extremally_disconnected iff Domains_Lattice X is B_Lattice )
proof end;