let X be non empty TopSpace; :: thesis: ( Closed_Domains_Lattice X = Open_Domains_Lattice X implies X is extremally_disconnected )
assume Closed_Domains_Lattice X = Open_Domains_Lattice X ; :: thesis: X is extremally_disconnected
then A1: Closed_Domains_of X = Open_Domains_of X ;
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 Closed_Domains_of X by A1;
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 Open_Domains_of X by A1;
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