theorem :: WAYBEL_5:2

for L being up-complete Semilattice holds
( L is continuous iff for x being Element of L ex I being Ideal of L st
( x <= sup I & ( for J being Ideal of L st x <= sup J holds
I c= J ) ) ) by Lm3, Lm4;