:: deftheorem defines is_<=_than LATTICE3:def 8 :
for A being RelStr
for X being set
for a being Element of A holds
( a is_<=_than X iff for b being Element of A st b in X holds
a <= b );