let L be up-complete Semilattice; :: thesis: ( L is continuous implies 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 ) ) )
assume A1: L is continuous ; :: thesis: 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 ) )
let x be Element of L; :: thesis: ex I being Ideal of L st
( x <= sup I & ( for J being Ideal of L st x <= sup J holds
I c= J ) )
reconsider I = waybelow x as Ideal of L by A1;
take I ; :: thesis: ( x <= sup I & ( for J being Ideal of L st x <= sup J holds
I c= J ) )
thus ( x <= sup I & ( for J being Ideal of L st x <= sup J holds
I c= J ) ) by A1, Lm1; :: thesis: verum