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 LemCastFunc02;
reconsider G1 = g1 as continuous Function of P,P ;
p = least_fix_point G1 by Deffixfunc, A1
.= sup (iter_min g) by Thfixpoint01 ;
hence p1 <= p by Lem201, A2; :: thesis: verum