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 Th39;
(D-Union Y) . (A,B) = (CLD-Union Y) . (A0,B0) by Th40;
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 Th42;
(D-Meet Y) . (A,B) = (OPD-Meet Y) . (A0,B0) by Th43;
hence (D-Meet Y) . (A,B) = A /\ B by TDLAT_1:def 11; :: thesis: verum