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