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 set ; :: according to TARSKI:def 3 :: thesis:
assume y in waybelow x ; :: thesis:
then y in { y' where y' is Element of L : y' << x } by WAYBEL_3:def 3;
then consider y' being Element of L such that
A2: ( y = y' & y' << x ) ;
thus y in I by A1, A2, WAYBEL_3:20; :: thesis:

end;

hence waybelow x c= I ; :: thesis:

end;