let L be up-complete Semilattice; :: 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 ) ) ) implies L is continuous )
assume A1: 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 ) ) ; :: thesis: L is continuous

now :: thesis: for x being Element of L holds
( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds
waybelow x c= I ) )

let x be Element of L; :: thesis: ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds
waybelow x c= I ) )
consider I being Ideal of L such that
A2: x <= sup I and
A3: for J being Ideal of L st x <= sup J holds
I c= J by A1;

now :: thesis: for y being object st y in I holds
y in waybelow x

let y be object ; :: thesis: ( y in I implies y in waybelow x )
assume A4: y in I ; :: thesis: y in waybelow x
then reconsider y9 = y as Element of L ;
for J being Ideal of L st x <= sup J holds
y in J

proof

let J be Ideal of L; :: thesis: ( x <= sup J implies y in J )
assume x <= sup J ; :: thesis: y in J
then I c= J by A3;
hence y in J by A4; :: thesis: verum

end;

then y9 << x by WAYBEL_3:21;
hence y in waybelow x by WAYBEL_3:7; :: thesis: verum

end;

then A5: I c= waybelow x ;
for y being object st y in waybelow x holds
y in I by A2, WAYBEL_3:7, WAYBEL_3:20;
then waybelow x c= I ;
then waybelow x = I by A5, XBOOLE_0:def 10;
hence ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds
waybelow x c= I ) ) by A2, A3; :: thesis: verum

end;

hence L is continuous by Lm2; :: thesis: verum