let L be Lattice; :: thesis: for D1, D2 being non empty Subset of
for D1', D2' being non empty Subset of holds
( D1 "\/" D2 = (D1 .: ) "/\" (D2 .: ) & (D1 .: ) "\/" (D2 .: ) = D1 "/\" D2 & D1' "\/" D2' = (.: D1') "/\" (.: D2') & (.: D1') "\/" (.: D2') = D1' "/\" D2' )
let D1, D2 be non empty Subset of ; :: thesis: for D1', D2' being non empty Subset of holds
( D1 "\/" D2 = (D1 .: ) "/\" (D2 .: ) & (D1 .: ) "\/" (D2 .: ) = D1 "/\" D2 & D1' "\/" D2' = (.: D1') "/\" (.: D2') & (.: D1') "\/" (.: D2') = D1' "/\" D2' )
let D1', D2' be non empty Subset of ; :: thesis: ( D1 "\/" D2 = (D1 .: ) "/\" (D2 .: ) & (D1 .: ) "\/" (D2 .: ) = D1 "/\" D2 & D1' "\/" D2' = (.: D1') "/\" (.: D2') & (.: D1') "\/" (.: D2') = D1' "/\" D2' )
A1: for L being Lattice
for D1, D2 being non empty Subset of holds D1 "\/" D2 = (D1 .: ) "/\" (D2 .: )

proof

let L be Lattice; :: thesis: for D1, D2 being non empty Subset of holds D1 "\/" D2 = (D1 .: ) "/\" (D2 .: )
let D1, D2 be non empty Subset of ; :: thesis: D1 "\/" D2 = (D1 .: ) "/\" (D2 .: )
thus D1 "\/" D2 c= (D1 .: ) "/\" (D2 .: ) :: according to XBOOLE_0:def 10 :: thesis: (D1 .: ) "/\" (D2 .: ) c= D1 "\/" D2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D1 "\/" D2 or x in (D1 .: ) "/\" (D2 .: ) )
assume x in D1 "\/" D2 ; :: thesis: x in (D1 .: ) "/\" (D2 .: )
then consider p, q being Element of such that
A2: ( x = p "\/" q & p in D1 & q in D2 ) ;
p "\/" q = (p .: ) "/\" (q .: ) ;
hence x in (D1 .: ) "/\" (D2 .: ) by A2; :: thesis: verum

end;

thus (D1 .: ) "/\" (D2 .: ) c= D1 "\/" D2 :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (D1 .: ) "/\" (D2 .: ) or x in D1 "\/" D2 )
assume x in (D1 .: ) "/\" (D2 .: ) ; :: thesis: x in D1 "\/" D2
then consider p', q' being Element of such that
A3: ( x = p' "/\" q' & p' in D1 & q' in D2 ) ;
(.: p') "\/" (.: q') = p' "/\" q' ;
hence x in D1 "\/" D2 by A3; :: thesis: verum

end;

end;

A4: ( (.: D1') .: = .: D1' & (.: D2') .: = .: D2' ) ;
( ((D1 .: ) .: ) "/\" ((D2 .: ) .: ) = D1 "/\" D2 & (D1' .: ) "/\" (D2' .: ) = (.: D1') "/\" (.: D2') ) by Lm2;
hence ( D1 "\/" D2 = (D1 .: ) "/\" (D2 .: ) & (D1 .: ) "\/" (D2 .: ) = D1 "/\" D2 & D1' "\/" D2' = (.: D1') "/\" (.: D2') & (.: D1') "\/" (.: D2') = D1' "/\" D2' ) by A1, A4; :: thesis: verum