let Y be non empty extremally_disconnected TopSpace; :: thesis: for A, B being Element of Domains_of Y holds
( (D-Union Y) . A,B = A \/ B & (D-Meet Y) . A,B = A /\ B )
let A, B be Element of Domains_of Y; :: thesis: ( (D-Union Y) . A,B = A \/ B & (D-Meet Y) . A,B = A /\ B )
reconsider A0 = A, B0 = B as Element of Closed_Domains_of Y by Th41;
(D-Union Y) . A,B = (CLD-Union Y) . A0,B0 by Th42;
hence (D-Union Y) . A,B = A \/ B by TDLAT_1:def 6; :: thesis: (D-Meet Y) . A,B = A /\ B
reconsider A0 = A, B0 = B as Element of Open_Domains_of Y by Th44;
(D-Meet Y) . A,B = (OPD-Meet Y) . A0,B0 by Th45;
hence (D-Meet Y) . A,B = A /\ B by TDLAT_1:def 11; :: thesis: verum