let L be non empty Chain; :: thesis: ( L is complete implies L is satisfying_axiom_of_approximation )
assume L is complete ; :: thesis: L is satisfying_axiom_of_approximation
then reconsider S = L as non empty complete Chain ;
S is satisfying_axiom_of_approximation

proof

let x be Element of S; :: according to WAYBEL_3:def 5 :: thesis: x = sup (waybelow x)
A1: ex_sup_of waybelow x,S by YELLOW_0:17;
A2: x is_>=_than waybelow x by Th9;

now

let y be Element of S; :: thesis: ( y is_>=_than waybelow x implies x <= y )
assume A3: ( y is_>=_than waybelow x & not x <= y ) ; :: thesis: contradiction
then ( x >= y & x <> y ) by WAYBEL_0:def 29;
then x > y by ORDERS_2:def 10;
then x >> y by Th13;
then y in waybelow x ;
then for z being Element of S st z is_>=_than waybelow x holds
z >= y by LATTICE3:def 9;
then A4: sup (waybelow x) = y by A1, A3, YELLOW_0:def 9;
x << x

proof

let D be non empty directed Subset of S; :: according to WAYBEL_3:def 1 :: thesis: ( x <= sup D implies ex d being Element of S st
( d in D & x <= d ) )
assume A5: x <= sup D ; :: thesis: ex d being Element of S st
( d in D & x <= d )
assume A6: for d being Element of S st d in D holds
not x <= d ; :: thesis: contradiction
A7: D c= waybelow x

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in D or a in waybelow x )
assume A8: a in D ; :: thesis: a in waybelow x
then reconsider a = a as Element of S ;
not x <= a by A6, A8;
then ( a <= x & a <> x ) by WAYBEL_0:def 29;
then a < x by ORDERS_2:def 10;
then a << x by Th13;
hence a in waybelow x ; :: thesis: verum

end;

ex_sup_of D,S by YELLOW_0:17;
then sup D <= sup (waybelow x) by A1, A7, YELLOW_0:34;
hence contradiction by A3, A4, A5, ORDERS_2:26; :: thesis: verum

end;

then x in waybelow x ;
hence contradiction by A3, LATTICE3:def 9; :: thesis: verum

end;

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

end;

hence L is satisfying_axiom_of_approximation ; :: thesis: verum