for P, Q being non empty strict chain-complete Poset
for f being Element of (ConPoset (P,Q)) st f = min_func (P,Q) holds
f is_<=_than the carrier of (ConPoset (P,Q))