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