let Y be non empty extremally_disconnected TopSpace; :: thesis: Domains_of Y = Open_Domains_of Y
now :: thesis: for S being object st S in Domains_of Y holds
S in Open_Domains_of Y
let S be object ; :: 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;
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 ; :: thesis: verum
end;
then A2: Domains_of Y c= Open_Domains_of Y ;
Open_Domains_of Y c= Domains_of Y by TDLAT_1:35;
hence Domains_of Y = Open_Domains_of Y by A2; :: thesis: verum