let P, Q be non empty strict chain-complete Poset; :: thesis: for f being Element of (ConPoset (P,Q)) st f = min_func (P,Q) holds
f is_<=_than the carrier of (ConPoset (P,Q))
let f be Element of (ConPoset (P,Q)); :: thesis: ( f = min_func (P,Q) implies f is_<=_than the carrier of (ConPoset (P,Q)) )
assume A1: f = min_func (P,Q) ; :: thesis: f is_<=_than the carrier of (ConPoset (P,Q))
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: f <= x
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: (min_func (P,Q)) . p <= g . p
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: ( q1 = (min_func (P,Q)) . p & q2 = g . p implies q1 <= q2 )
assume ( q1 = (min_func (P,Q)) . p & q2 = g . p ) ; :: thesis: q1 <= q2
then q1 = Bottom Q by FUNCOP_1:7;
hence q1 <= q2 by YELLOW_0:44; :: thesis: verum

end;

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

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: verum

end;

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