theorem Th30: :: LATTICE3:30

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