theorem Th37: :: LATTICE2:37

for L being Lattice
for a, b being Element of L
for a9, b9 being Element of (L .:) st a = a9 & b = b9 holds
( a "/\" b = a9 "\/" b9 & a "\/" b = a9 "/\" b9 ) ;