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 B1: 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);
set M = f .: L;
C2: sup (f .: L) <= f . (sup L) by Thmonotone02;
f . (sup L) <= sup (f .: L) by B1;
hence f . (sup L) = sup (f .: L) by ORDERS_2:25, C2; :: thesis: verum

end;

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