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

end;

end;

A4: ( LattStr(# the carrier of L,the L_join of L,the L_meet of L #) = (L .: ) .: & D1 .: = D1 & (D1 .: ) .: = D1 .: & D2 .: = D2 & (D2 .: ) .: = D2 .: & .: D1' = D1' & (.: D1') .: = .: D1' & .: D2' = D2' & (.: D2') .: = .: D2' & 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