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 A0: 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 A1: p is_a_fixpoint_of g ; :: thesis: p4 <= p
set M = iter_min g;
set a = Bottom P;
A2: ex_sup_of iter_min g,P by DefchainComplete;
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
B1: ( p1 = p2 & ex n being Nat st p2 = (iter (g,n)) . (Bottom P) ) ;
consider n being Nat such that
B2: p1 = (iter (g,n)) . (Bottom P) by B1;
reconsider q = (iter (g,n)) . p as Element of P by Lemiter11;
p1 <= q by B2, YELLOW_0:44, Lemiter13;
hence p1 <= p by A1, Lemiter16; :: thesis: verum

end;

then iter_min g is_<=_than p by LATTICE3:def 9;
hence p4 <= p by A2, YELLOW_0:def 9, A0; :: thesis: verum

end;

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