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
B1: ( x = x1 & ex g being continuous Function of P,Q st g = x1 ) ;
consider g being continuous Function of P,Q such that
B2: g = x1 by B1;
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:13;
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:10;
then [f,x] in ConRelat P,Q by B1, B2, DefConRelat, A1;
hence f <= x by ORDERS_2:def 9; :: thesis: verum

end;

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