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
now :: thesis: for x being Element of L holds x = sup (waybelow x)
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;
then A4: L is satisfying_axiom_of_approximation by WAYBEL_3:def 5;
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