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