thus for x being Element of [:S,T:] holds
( not compactbelow x is empty & compactbelow x is directed ) ; :: according to WAYBEL_8:def 4 :: thesis: ( [:S,T:] is up-complete & [:S,T:] is satisfying_axiom_K )
thus ( [:S,T:] is up-complete & [:S,T:] is satisfying_axiom_K ) ; :: thesis: verum