thus for x being Element of [:S,T:] holds
( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def 6 :: thesis: ( [:S,T:] is up-complete & [:S,T:] is satisfying_axiom_of_approximation )
thus ( [:S,T:] is up-complete & [:S,T:] is satisfying_axiom_of_approximation ) ; :: thesis: verum