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:8;
g1 in ConFuncs (P,P) by A1;
hence g is Element of (ConPoset (P,P)) ; :: thesis: verum