let P, Q be non empty strict chain-complete Poset; :: thesis: min_func (P,Q) is Element of (ConPoset (P,Q))
reconsider f = min_func (P,Q) as continuous Function of P,Q ;
reconsider x = f as Element of Funcs ( the carrier of P, the carrier of Q) by FUNCT_2:8;
x in ConFuncs (P,Q) ;
hence min_func (P,Q) is Element of (ConPoset (P,Q)) ; :: thesis: verum