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.>).> )
A1: ( (.(D1 \/ (.D2.>).> = <.((D1 \/ (.D2.>) .:).) & (.D2.> = <.(D2 .:).) ) by Th36;
A2: (.(D1 \/ D2).> = <.((D1 \/ D2) .:).) by Th36;
( (.((.D1.> \/ D2).> = <.(((.D1.> \/ D2) .:).) & (.D1.> = <.(D1 .:).) ) by Th36;
hence ( (.(D1 \/ D2).> = (.((.D1.> \/ D2).> & (.(D1 \/ D2).> = (.(D1 \/ (.D2.>).> ) by A1, A2, FILTER_0:34; :: thesis: verum