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 object ; :: 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 object ; :: 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 Lm3;
hence ( D1 "\/" D2 = (D1 .:) "/\" (D2 .:) & (D1 .:) "\/" (D2 .:) = D1 "/\" D2 & D19 "\/" D29 = (.: D19) "/\" (.: D29) & (.: D19) "\/" (.: D29) = D19 "/\" D29 ) by A1, A4; :: thesis: verum