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

proof

assume A1: f is continuous ; :: thesis: ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) )
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)
B1: f preserves_sup_of L by A1, Defcontinuous;
ex_sup_of L,P by DefchainComplete;
hence f . (sup L) = sup (f .: L) by WAYBEL_0:def 31, B1; :: thesis: verum

end;

hence ( f is monotone & ( for L being non empty Chain of P holds f . (sup L) = sup (f .: L) ) ) by A1, Defcontinuous; :: thesis: verum

end;

assume that
B1: f is monotone and
B2: 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 preserves_sup_of L

proof

let L be non empty Chain of P; :: thesis: f preserves_sup_of L
reconsider M = f .: L as non empty Chain of Q by B1, ThChain1;
( ex_sup_of M,Q & f . (sup L) = sup M ) by DefchainComplete, B2;
hence f preserves_sup_of L by WAYBEL_0:def 31; :: thesis: verum

end;

hence f is continuous by B1, Defcontinuous; :: thesis: verum