theorem Th9: :: LATTICE5:9

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