let L1, L2 be Lattice; 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; for p2, q2 being Element of L2 holds
( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )
let p2, q2 be Element of L2; ( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )
thus
( [p1,p2] [= [q1,q2] implies ( p1 [= q1 & p2 [= q2 ) )
( p1 [= q1 & p2 [= q2 implies [p1,p2] [= [q1,q2] )
assume that
A1:
p1 "\/" q1 = q1
and
A2:
p2 "\/" q2 = q2
; LATTICES:def 3 [p1,p2] [= [q1,q2]
thus
[p1,p2] "\/" [q1,q2] = [q1,q2]
by A1, A2, Th21; LATTICES:def 3 verum