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:8;
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