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

let I be Ideal of L; :: thesis:
assume A1: x <= sup I ; :: thesis:
waybelow x c= I

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in waybelow x ; :: thesis:
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 A1, WAYBEL_3:20; :: thesis:

end;

hence waybelow x c= I ; :: thesis:

end;