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

proof

let L be Lattice; :: thesis: for D1, D2 being non empty Subset of L holds D1 "\/" D2 = (D1 .: ) "/\" (D2 .: )
let D1, D2 be non empty Subset of L; :: 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 L 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 p9, q9 being Element of (L .: ) such that
A3: ( x = p9 "/\" q9 & p9 in D1 & q9 in D2 ) ;
(.: p9) "\/" (.: q9) = p9 "/\" q9 ;
hence x in D1 "\/" D2 by A3; :: thesis: verum

end;

end;

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