let x be set ; :: thesis: for P being non empty strict chain-complete Poset st x is Element of (ConPoset (P,P)) holds
x is continuous Function of P,P
let P be non empty strict chain-complete Poset; :: thesis: ( x is Element of (ConPoset (P,P)) implies x is continuous Function of P,P )
assume x is Element of (ConPoset (P,P)) ; :: thesis: x is continuous Function of P,P
then x in ConFuncs (P,P) ;
then consider y being Element of Funcs ( the carrier of P, the carrier of P) such that
A1: ( x = y & ex g being continuous Function of P,P st g = y ) ;
thus x is continuous Function of P,P by A1; :: thesis: verum