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

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

let y be set ; :: 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 by TARSKI:def 3;

now

let y be set ; :: thesis: ( y in waybelow x implies y in I )
assume A6: y in waybelow x ; :: thesis: y in I
then reconsider y9 = y as Element of L ;
y9 << x by A6, WAYBEL_3:7;
hence y in I by A2, WAYBEL_3:20; :: thesis: verum

end;

then waybelow x c= I by TARSKI:def 3;
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