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

now :: thesis: for S being object st S in Domains_of Y holds
S in Closed_Domains_of Y

let S be object ; :: thesis: ( S in Domains_of Y implies S in Closed_Domains_of Y )
assume A1: S in Domains_of Y ; :: thesis: S in Closed_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 closed_condensed by Th33;
then A in { E where E is Subset of Y : E is closed_condensed } ;
hence S in Closed_Domains_of Y ; :: thesis: verum

end;

then A2: Domains_of Y c= Closed_Domains_of Y ;
Closed_Domains_of Y c= Domains_of Y by TDLAT_1:31;
hence Domains_of Y = Closed_Domains_of Y by A2; :: thesis: verum