let L1, L2 be Lattice; :: thesis: for p1, q1 being Element of L1
for p2, q2 being Element of L2 holds
( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )
let p1, q1 be Element of L1; :: thesis: for p2, q2 being Element of L2 holds
( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )
let p2, q2 be Element of L2; :: thesis: ( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )
thus ( [p1,p2] [= [q1,q2] implies ( p1 [= q1 & p2 [= q2 ) ) :: thesis: ( p1 [= q1 & p2 [= q2 implies [p1,p2] [= [q1,q2] )

proof

assume [p1,p2] "\/" [q1,q2] = [q1,q2] ; :: according to LATTICES:def 3 :: thesis: ( p1 [= q1 & p2 [= q2 )
then [(p1 "\/" q1),(p2 "\/" q2)] = [q1,q2] by Th21;
hence ( p1 "\/" q1 = q1 & p2 "\/" q2 = q2 ) by XTUPLE_0:1; :: according to LATTICES:def 3 :: thesis: verum

end;

assume that
A1: p1 "\/" q1 = q1 and
A2: p2 "\/" q2 = q2 ; :: according to LATTICES:def 3 :: thesis: [p1,p2] [= [q1,q2]
thus [p1,p2] "\/" [q1,q2] = [q1,q2] by A1, A2, Th21; :: according to LATTICES:def 3 :: thesis: verum