let L be Lattice; :: thesis: for D1, D2 being non empty Subset of L holds
( (.(D1 \/ D2).> = (.((.D1.> \/ D2).> & (.(D1 \/ D2).> = (.(D1 \/ (.D2.>).> )
let D1, D2 be non empty Subset of L; :: thesis: ( (.(D1 \/ D2).> = (.((.D1.> \/ D2).> & (.(D1 \/ D2).> = (.(D1 \/ (.D2.>).> )
( (.((.D1.> \/ D2).> = <.(((.D1.> \/ D2) .: ).) & (.D1.> = <.(D1 .: ).) & (.(D1 \/ (.D2.>).> = <.((D1 \/ (.D2.>) .: ).) & (.D2.> = <.(D2 .: ).) & (.(D1 \/ D2).> = <.((D1 \/ D2) .: ).) & (D1 \/ (.D2.>) .: = D1 \/ (.D2.> & (D1 \/ D2) .: = D1 \/ D2 & D1 .: = D1 & D2 .: = D2 & ((.D1.> \/ D2) .: = (.D1.> \/ D2 & (.D1.> .: = (.D1.> & (.D2.> .: = (.D2.> ) by Th37;
hence ( (.(D1 \/ D2).> = (.((.D1.> \/ D2).> & (.(D1 \/ D2).> = (.(D1 \/ (.D2.>).> ) by FILTER_0:47; :: thesis: verum