let L be continuous Semilattice; :: 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 ) )

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

thus x <= sup () by WAYBEL_3:def 5; :: thesis: for I being Ideal of L st x <= sup I holds
waybelow x c= I

thus for I being Ideal of L st x <= sup I holds
waybelow x c= I :: thesis: verum
proof
let I be Ideal of L; :: thesis: ( x <= sup I implies waybelow x c= I )
assume A1: x <= sup I ; :: thesis:
waybelow x c= I
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in waybelow x or y in I )
assume y in waybelow x ; :: thesis: y in I
then y in { y9 where y9 is Element of L : y9 << x } by WAYBEL_3:def 3;
then ex y9 being Element of L st
( y = y9 & y9 << x ) ;
hence y in I by ; :: thesis: verum
end;
hence waybelow x c= I ; :: thesis: verum
end;