for L1, L2 being Lattice
for p1, q1 being Element of L1
for p2, q2 being Element of L2 holds
( [p1,p2] "\/" [q1,q2] = [(p1 "\/" q1),(p2 "\/" q2)] & [p1,p2] "/\" [q1,q2] = [(p1 "/\" q1),(p2 "/\" q2)] ) by Th21;