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

now

let S be set ; :: 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, TDLAT_1:def 1;
then ex D being Subset of Y st
( D = A & D is condensed ) ;
then A is closed_condensed by Th35;
then A in { E where E is Subset of Y : E is closed_condensed } ;
hence S in Closed_Domains_of Y by TDLAT_1:def 5; :: thesis: verum

end;

then A2: Domains_of Y c= Closed_Domains_of Y by TARSKI:def 3;
Closed_Domains_of Y c= Domains_of Y by TDLAT_1:31;
hence Domains_of Y = Closed_Domains_of Y by A2, XBOOLE_0:def 10; :: thesis: verum