let Y be non empty extremally_disconnected TopSpace; :: thesis: Domains_of Y = Open_Domains_of Y

now

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 consider D being Subset of Y such that
A2: ( D = A & D is condensed ) ;
A is open_condensed by A2, Th35;
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 ( Domains_of Y c= Open_Domains_of Y & Open_Domains_of Y c= Domains_of Y ) by TARSKI:def 3, TDLAT_1:35;
hence Domains_of Y = Open_Domains_of Y by XBOOLE_0:def 10; :: thesis: verum