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:11;
x in ConFuncs P,Q ;
hence min_func P,Q is Element of (ConPoset P,Q) ; :: thesis: verum