let L be up-complete Semilattice; :: thesis: ( ( for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ) implies ( L is satisfying_axiom_of_approximation iff for x, y being Element of L st not x <= y holds
ex u being Element of L st
( u << x & not u <= y ) ) )
assume A1: for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ; :: thesis: ( L is satisfying_axiom_of_approximation iff for x, y being Element of L st not x <= y holds
ex u being Element of L st
( u << x & not u <= y ) )

hereby :: thesis: ( ( for x, y being Element of L st not x <= y holds
ex u being Element of L st
( u << x & not u <= y ) ) implies L is satisfying_axiom_of_approximation )

assume A2: L is satisfying_axiom_of_approximation ; :: thesis: for x, y being Element of L st not x <= y holds
ex u being Element of L st
( u << x & not u <= y )
let x, y be Element of L; :: thesis: ( not x <= y implies ex u being Element of L st
( u << x & not u <= y ) )
assume A3: not x <= y ; :: thesis: ex u being Element of L st
( u << x & not u <= y )
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: ( u << x & not u <= y )
thus ( u << x & not u <= y ) by A6, A7, Th7; :: thesis: verum

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: L is satisfying_axiom_of_approximation
let x be Element of L; :: according to WAYBEL_3:def 5 :: thesis: x = sup (waybelow x)
( 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;

now :: thesis: for y being Element of L st y is_>=_than waybelow x holds
x <= y

let y be Element of L; :: thesis: ( y is_>=_than waybelow x implies x <= y )
assume that
A11: y is_>=_than waybelow x and
A12: not x <= y ; :: thesis: contradiction
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: verum

end;

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