let P be non empty strict chain-complete Poset; :: thesis: for g being monotone Function of P,P st g is continuous Function of P,P holds
g is Element of (ConPoset P,P)
let g be monotone Function of P,P; :: thesis: ( g is continuous Function of P,P implies g is Element of (ConPoset P,P) )
assume A1: g is continuous Function of P,P ; :: thesis: g is Element of (ConPoset P,P)
reconsider g1 = g as Element of Funcs the carrier of P,the carrier of P by FUNCT_2:11;
g1 in ConFuncs P,P by A1;
hence g is Element of (ConPoset P,P) ; :: thesis: verum