let P, Q be non empty strict chain-complete Poset; :: thesis:
let f be Element of (ConPoset (P,Q)); :: thesis:
assume A1: f = min_func (P,Q) ; :: thesis:
set f1 = min_func (P,Q);
for x being Element of (ConPoset (P,Q)) holds f <= x

proof

let x be Element of (ConPoset (P,Q)); :: thesis:
x in ConFuncs (P,Q) ;
then consider x1 being Element of Funcs ( the carrier of P, the carrier of Q) such that
A2: ( x = x1 & ex g being continuous Function of P,Q st g = x1 ) ;
consider g being continuous Function of P,Q such that
A3: g = x1 by A2;
for p being Element of P holds (min_func (P,Q)) . p <= g . p

proof

let p be Element of P; :: thesis:
for q1, q2 being Element of Q st q1 = (min_func (P,Q)) . p & q2 = g . p holds
q1 <= q2

proof

let q1, q2 be Element of Q; :: thesis:
assume ( q1 = (min_func (P,Q)) . p & q2 = g . p ) ; :: thesis:
then q1 = Bottom Q by FUNCOP_1:7;
hence q1 <= q2 by YELLOW_0:44; :: thesis:

end;

hence (min_func (P,Q)) . p <= g . p ; :: thesis:

end;

then min_func (P,Q) <= g by YELLOW_2:9;
then [f,x] in ConRelat (P,Q) by A2, A3, Def7, A1;
hence f <= x by ORDERS_2:def 5; :: thesis:

end;

hence f is_<=_than the carrier of (ConPoset (P,Q)) ; :: thesis: