let L be 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 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 :: thesis: for y being Element of S st y is_>=_than waybelow x holds
x <= y

let y be Element of S; :: thesis: ( y is_>=_than waybelow x implies x <= y )
assume that
A3: y is_>=_than waybelow x and
A4: not x <= y ; :: thesis: contradiction
x >= y by A4, WAYBEL_0:def 29;
then x > y by A4;
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 ;
then A5: 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 A6: x <= sup D ; :: thesis: ex d being Element of S st
( d in D & x <= d )
assume A7: for d being Element of S st d in D holds
not x <= d ; :: thesis: contradiction
A8: D c= waybelow x

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in D or a in waybelow x )
assume A9: a in D ; :: thesis: a in waybelow x
then reconsider a = a as Element of S ;
A10: not x <= a by A7, A9;
then a <= x by WAYBEL_0:def 29;
then a < x by A10;
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, A8, YELLOW_0:34;
hence contradiction by A4, A5, A6, ORDERS_2:3; :: thesis: verum

end;

then x in waybelow x ;
hence contradiction by A3, A4; :: 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