let Y be non empty extremally_disconnected TopSpace; :: thesis: Domains_Lattice Y = Open_Domains_Lattice Y
A1: D-Union Y = OPD-Union Y by Th45;
A2: D-Meet Y = OPD-Meet Y by Th45;
Domains_of Y = Open_Domains_of Y by Th44;
hence Domains_Lattice Y = LattStr(# (Open_Domains_of Y),(OPD-Union Y),(OPD-Meet Y) #) by A1, A2, TDLAT_1:def 4
.= Open_Domains_Lattice Y by TDLAT_1:def 12 ;
:: thesis: verum