let P, Q be non empty strict chain-complete Poset; :: thesis: for f being monotone Function of P,Q st ( for L being non empty Chain of P holds f . (sup L) <= sup (f .: L) ) holds
f is continuous
let f be monotone Function of P,Q; :: thesis: ( ( for L being non empty Chain of P holds f . (sup L) <= sup (f .: L) ) implies f is continuous )
assume A1: for L being non empty Chain of P holds f . (sup L) <= sup (f .: L) ; :: thesis: f is continuous
for L being non empty Chain of P holds f . (sup L) = sup (f .: L)

proof

let L be non empty Chain of P; :: thesis: f . (sup L) = sup (f .: L)
set a1 = f . (sup L);
set a2 = sup (f .: L);
A2: sup (f .: L) <= f . (sup L) by Th2;
f . (sup L) <= sup (f .: L) by A1;
hence f . (sup L) = sup (f .: L) by A2, ORDERS_2:2; :: thesis: verum

end;

hence f is continuous by Th6; :: thesis: verum