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

( 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