theorem Th31: :: LATTICE3:31

for X being set
for L being Lattice
for p9 being Element of (LattPOSet L) holds
( X is_<=_than p9 iff X is_less_than % p9 )