let L be non empty reflexive RelStr ; :: thesis: ( L is trivial implies L is satisfying_axiom_of_approximation )
assume for x, y being Element of L holds x = y ; :: according to STRUCT_0:def 10 :: thesis: L is satisfying_axiom_of_approximation
hence for x being Element of L holds x = sup (waybelow x) ; :: according to WAYBEL_3:def 5 :: thesis: verum