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 () & ( 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 () & ( 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:
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 ;
then waybelow x c= I ;
then waybelow x = I by ;
hence ( waybelow x is Ideal of L & x <= sup () & ( 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