let L be 1 -element reflexive RelStr ; :: thesis: L is satisfying_axiom_of_approximation
thus for x being Element of L holds x = sup (waybelow x) by ZFMISC_1:def 10; :: according to WAYBEL_3:def 5 :: thesis: verum