let L be Chain; :: thesis:
assume L is complete ; :: thesis:
then reconsider S = L as complete Chain ;
S is satisfying_axiom_of_approximation

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

let y be Element of S; :: thesis:
assume that
A3: y is_>=_than waybelow x and
A4: not x <= y ; :: thesis:
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

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

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A9: a in D ; :: thesis:
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:

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:

end;

then x in waybelow x ;
hence contradiction by A3, A4; :: thesis:

end;

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

end;

hence L is satisfying_axiom_of_approximation ; :: thesis: