let P be non empty strict chain-complete Poset; :: thesis: for p4 being Element of P
for g being monotone Function of P,P st p4 = sup (iter_min g) holds
for p being Element of P st p is_a_fixpoint_of g holds
p4 <= p
let p4 be Element of P; :: thesis: for g being monotone Function of P,P st p4 = sup (iter_min g) holds
for p being Element of P st p is_a_fixpoint_of g holds
p4 <= p
let g be monotone Function of P,P; :: thesis: ( p4 = sup (iter_min g) implies for p being Element of P st p is_a_fixpoint_of g holds
p4 <= p )
assume A1: p4 = sup (iter_min g) ; :: thesis: for p being Element of P st p is_a_fixpoint_of g holds
p4 <= p
for p being Element of P st p is_a_fixpoint_of g holds
p4 <= p

proof

let p be Element of P; :: thesis: ( p is_a_fixpoint_of g implies p4 <= p )
assume A2: p is_a_fixpoint_of g ; :: thesis: p4 <= p
set M = iter_min g;
set a = Bottom P;
A3: ex_sup_of iter_min g,P by Def1;
for p1 being Element of P st p1 in iter_min g holds
p1 <= p

proof

let p1 be Element of P; :: thesis: ( p1 in iter_min g implies p1 <= p )
assume p1 in iter_min g ; :: thesis: p1 <= p
then consider p2 being Element of P such that
A4: ( p1 = p2 & ex n being Nat st p2 = (iter (g,n)) . (Bottom P) ) ;
consider n being Nat such that
A5: p1 = (iter (g,n)) . (Bottom P) by A4;
reconsider q = (iter (g,n)) . p as Element of P ;
p1 <= q by A5, Lm3, YELLOW_0:44;
hence p1 <= p by A2, Lm6; :: thesis: verum

end;

then iter_min g is_<=_than p ;
hence p4 <= p by A3, A1, YELLOW_0:def 9; :: thesis: verum

end;

hence for p being Element of P st p is_a_fixpoint_of g holds
p4 <= p ; :: thesis: verum