let P be non empty strict chain-complete Poset; :: thesis: for g being continuous Function of P,P
for p, p1 being Element of P
for n being Nat st p = (fix_func P) . g & p1 = (iter (g,n)) . (Bottom P) holds
p1 <= p
let g be continuous Function of P,P; :: thesis: for p, p1 being Element of P
for n being Nat st p = (fix_func P) . g & p1 = (iter (g,n)) . (Bottom P) holds
p1 <= p
let p, p1 be Element of P; :: thesis: for n being Nat st p = (fix_func P) . g & p1 = (iter (g,n)) . (Bottom P) holds
p1 <= p
let n be Nat; :: thesis: ( p = (fix_func P) . g & p1 = (iter (g,n)) . (Bottom P) implies p1 <= p )
set a = Bottom P;
assume A1: ( p = (fix_func P) . g & p1 = (iter (g,n)) . (Bottom P) ) ; :: thesis: p1 <= p
then A2: p1 in iterSet (g,(Bottom P)) ;
reconsider g1 = g as Element of (ConPoset (P,P)) by Lm25;
reconsider G1 = g1 as continuous Function of P,P ;
p = least_fix_point G1 by Def12, A1
.= sup (iter_min g) by Th9 ;
hence p1 <= p by Lm18, A2; :: thesis: verum