:: deftheorem defines is_less_than LATTICE3:def 17 :
for L being non empty LattStr
for p being Element of L
for X being set holds
( X is_less_than p iff for q being Element of L st q in X holds
q [= p );