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