let L be up-complete Semilattice; :: thesis: ( ( for x being Element of L holds

( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds

waybelow x c= I ) ) ) implies L is continuous )

assume A1: for x being Element of L holds

( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds

waybelow x c= I ) ) ; :: thesis: L is continuous

for x being Element of L holds

( not waybelow x is empty & waybelow x is directed ) by A1;

hence L is continuous by A4, WAYBEL_3:def 6; :: thesis: verum

( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds

waybelow x c= I ) ) ) implies L is continuous )

assume A1: for x being Element of L holds

( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds

waybelow x c= I ) ) ; :: thesis: L is continuous

now :: thesis: for x being Element of L holds x = sup (waybelow x)

then A4:
L is satisfying_axiom_of_approximation
by WAYBEL_3:def 5;let x be Element of L; :: thesis: x = sup (waybelow x)

A2: x <= sup (waybelow x) by A1;

( not waybelow x is empty & waybelow x is directed ) by A1;

then A3: ex_sup_of waybelow x,L by WAYBEL_0:75;

waybelow x is_<=_than x by WAYBEL_3:9;

then sup (waybelow x) <= x by A3, YELLOW_0:def 9;

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

end;A2: x <= sup (waybelow x) by A1;

( not waybelow x is empty & waybelow x is directed ) by A1;

then A3: ex_sup_of waybelow x,L by WAYBEL_0:75;

waybelow x is_<=_than x by WAYBEL_3:9;

then sup (waybelow x) <= x by A3, YELLOW_0:def 9;

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

for x being Element of L holds

( not waybelow x is empty & waybelow x is directed ) by A1;

hence L is continuous by A4, WAYBEL_3:def 6; :: thesis: verum