theorem :: WAYBEL_3:24

for L being up-complete Semilattice st ( for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ) holds
( L is satisfying_axiom_of_approximation iff for x, y being Element of L st not x <= y holds
ex u being Element of L st
( u << x & not u <= y ) )