:: deftheorem Def5 defines satisfying_axiom_of_approximation WAYBEL_3:def 5 :
for L being non empty reflexive RelStr holds
( L is satisfying_axiom_of_approximation iff for x being Element of L holds x = sup (waybelow x) );