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
A2: ( 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 A2; :: thesis: verum