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:
( not waybelow x is empty & waybelow x is directed ) by A1;
then ( x = sup (waybelow x) & ex_sup_of waybelow x,L ) by A2, Def5, WAYBEL_0:75;
then ( y is_>=_than waybelow x implies y >= x ) by YELLOW_0:def 9;
then consider u being Element of L such that
A4: ( u in waybelow x & not u <= y ) by A3, LATTICE3:def 9;
take u = u; :: thesis:
thus ( u << x & not u <= y ) by A4, Th7; :: thesis:

end;

assume A5: 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 A6: ex_sup_of waybelow x,L by WAYBEL_0:75;
A7: x is_>=_than waybelow x by Th9;

let y be Element of L; :: thesis:
assume A8: ( y is_>=_than waybelow x & not x <= y ) ; :: thesis:
then consider u being Element of L such that
A9: ( u << x & not u <= y ) by A5;
u in waybelow x by A9;
hence contradiction by A8, A9, LATTICE3:def 9; :: thesis:

end;

hence x = sup (waybelow x) by A6, A7, YELLOW_0:def 9; :: thesis: