theorem Th7: :: LATTICE5:7

for L being Lattice
for a, b being Element of (LattPOSet L) holds a "/\" b = (% a) "/\" (% b)