let P, Q be non empty strict chain-complete Poset; :: thesis: for F being non empty Chain of (ConPoset P,Q) holds sup_func F is Element of (ConPoset P,Q)
let F be non empty Chain of (ConPoset P,Q); :: thesis: sup_func F is Element of (ConPoset P,Q)
set x = sup_func F;
A1: sup_func F is Element of Funcs the carrier of P,the carrier of Q by FUNCT_2:11;
reconsider x = sup_func F as continuous Function of P,Q ;
x in ConFuncs P,Q by A1;
hence sup_func F is Element of (ConPoset P,Q) ; :: thesis: verum