let L be up-complete Semilattice; :: thesis:
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:

let x be Element of L; :: thesis:
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;

let y be object ; :: thesis:
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

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

end;

end;

end;