let Y be non empty extremally_disconnected TopSpace; 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; ( (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; (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; verum