let P be non empty strict chain-complete Poset; :: thesis: for g1, g2 being monotone Function of P,P st g1 <= g2 holds
sup (iter_min g1) <= sup (iter_min g2)
let g1, g2 be monotone Function of P,P; :: thesis: ( g1 <= g2 implies sup (iter_min g1) <= sup (iter_min g2) )
assume A1: g1 <= g2 ; :: thesis: sup (iter_min g1) <= sup (iter_min g2)
set p2 = sup (iter_min g2);
set a = Bottom P;
A2: ( ex_sup_of iter_min g1,P & ex_sup_of iter_min g2,P ) by Def1;
then A3: iter_min g2 is_<=_than sup (iter_min g2) by YELLOW_0:def 9;
for x being Element of P st x in iter_min g1 holds
x <= sup (iter_min g2)

proof

let x be Element of P; :: thesis: ( x in iter_min g1 implies x <= sup (iter_min g2) )
assume x in iter_min g1 ; :: thesis: x <= sup (iter_min g2)
then consider p being Element of P such that
A4: ( x = p & ex n being Nat st p = (iter (g1,n)) . (Bottom P) ) ;
consider n being Nat such that
A5: p = (iter (g1,n)) . (Bottom P) by A4;
reconsider y = (iter (g2,n)) . (Bottom P) as Element of P ;
y in iter_min g2 ;
then A6: y <= sup (iter_min g2) by A3;
p <= y by A1, A5, Lm7;
hence x <= sup (iter_min g2) by A4, A6, ORDERS_2:3; :: thesis: verum

end;

then iter_min g1 is_<=_than sup (iter_min g2) ;
hence sup (iter_min g1) <= sup (iter_min g2) by A2, YELLOW_0:30; :: thesis: verum