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