:: deftheorem Def17 defines approximating WAYBEL_4:def 17 :
for L being non empty RelStr
for AR being Relation of L holds
( AR is approximating iff for x being Element of L holds x = sup (AR -below x) );