let L be up-complete Semilattice; :: thesis:
assume A1: for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ; :: thesis:

hereby :: thesis:

assume A2: L is satisfying_axiom_of_approximation ; :: thesis:
let x, y be Element of L; :: thesis:
assume A3: not x <= y ; :: thesis:
A4: ( not waybelow x is empty & waybelow x is directed ) by A1;
A5: x = sup (waybelow x) by A2;
ex_sup_of waybelow x,L by A4, WAYBEL_0:75;
then ( y is_>=_than waybelow x implies y >= x ) by A5, YELLOW_0:def 9;
then consider u being Element of L such that
A6: u in waybelow x and
A7: not u <= y by A3;
take u = u; :: thesis:
thus ( u << x & not u <= y ) by A6, A7, Th7; :: thesis:

end;

assume A8: for x, y being Element of L st not x <= y holds
ex u being Element of L st
( u << x & not u <= y ) ; :: thesis:
let x be Element of L; :: according to WAYBEL_3:def 5 :: thesis:
( not waybelow x is empty & waybelow x is directed ) by A1;
then A9: ex_sup_of waybelow x,L by WAYBEL_0:75;
A10: x is_>=_than waybelow x by Th9;

let y be Element of L; :: thesis:
assume that
A11: y is_>=_than waybelow x and
A12: not x <= y ; :: thesis:
consider u being Element of L such that
A13: u << x and
A14: not u <= y by A8, A12;
u in waybelow x by A13;
hence contradiction by A11, A14; :: thesis:

end;

hence x = sup (waybelow x) by A9, A10, YELLOW_0:def 9; :: thesis: