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