let Y be non empty extremally_disconnected TopSpace; :: thesis: Domains_Lattice Y = Closed_Domains_Lattice Y
A1: D-Union Y = CLD-Union Y by Th40;
A2: D-Meet Y = CLD-Meet Y by Th40;
Domains_of Y = Closed_Domains_of Y by Th39;
hence Domains_Lattice Y = LattStr(# (Closed_Domains_of Y),(CLD-Union Y),(CLD-Meet Y) #) by A1, A2, TDLAT_1:def 4
.= Closed_Domains_Lattice Y by TDLAT_1:def 8 ;
:: thesis: verum