let Y be non empty extremally_disconnected TopSpace; :: thesis: ( D-Union Y = OPD-Union Y & D-Meet Y = OPD-Meet Y )
A1: Domains_of Y = Open_Domains_of Y by Th42;
hence D-Union Y = (D-Union Y) || (Open_Domains_of Y) by RELSET_1:19
.= OPD-Union Y by TDLAT_1:42 ;
:: thesis: D-Meet Y = OPD-Meet Y
thus D-Meet Y = (D-Meet Y) || (Open_Domains_of Y) by A1, RELSET_1:19
.= OPD-Meet Y by TDLAT_1:43 ; :: thesis: verum