let Y be non empty extremally_disconnected TopSpace; :: thesis: ( D-Union Y = CLD-Union Y & D-Meet Y = CLD-Meet Y )
A1: Domains_of Y = Closed_Domains_of Y by Th39;
hence D-Union Y = (D-Union Y) || (Closed_Domains_of Y) by RELSET_1:19
.= CLD-Union Y by TDLAT_1:39 ;
:: thesis: D-Meet Y = CLD-Meet Y
thus D-Meet Y = (D-Meet Y) || (Closed_Domains_of Y) by A1, RELSET_1:19
.= CLD-Meet Y by TDLAT_1:40 ; :: thesis: verum