let L be complete LATTICE; :: thesis: ( ( for x being Element of L holds x is compact ) implies L is satisfying_axiom_of_approximation )
assume A1: for x being Element of L holds x is compact ; :: thesis: L is satisfying_axiom_of_approximation
let x be Element of L; :: according to WAYBEL_3:def 5 :: thesis: x = sup (waybelow x)
x is compact by A1;
then x << x ;
then A2: x in waybelow x ;
waybelow x is_<=_than sup (waybelow x) by YELLOW_0:32;
then A3: x <= sup (waybelow x) by A2;
A4: ex_sup_of waybelow x,L by YELLOW_0:17;
A5: ex_sup_of downarrow x,L by WAYBEL_0:34;
sup (downarrow x) = x by WAYBEL_0:34;
then x >= sup (waybelow x) by A4, A5, Th11, YELLOW_0:34;
hence x = sup (waybelow x) by A3, ORDERS_2:2; :: thesis: verum