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 Th22;
hence ( p1 "\/" q1 = q1 & p2 "\/" q2 = q2 ) by ZFMISC_1:33; :: according to LATTICES:def 3 :: thesis: verum

end;

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