let L be lower-bounded sup-Semilattice; :: thesis: ( L is up-complete & L is satisfying_axiom_of_approximation implies L is continuous )
assume A1: ( L is up-complete & L is satisfying_axiom_of_approximation ) ; :: thesis: L is continuous
thus for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def 6 :: thesis: ( L is up-complete & L is satisfying_axiom_of_approximation )
thus ( L is up-complete & L is satisfying_axiom_of_approximation ) by A1; :: thesis: verum