let P be non empty strict chain-complete Poset; :: thesis: for p being Element of P
for g being monotone Function of P,P st g is continuous & p = sup (iter_min g) holds
p is_a_fixpoint_of g
let p be Element of P; :: thesis: for g being monotone Function of P,P st g is continuous & p = sup (iter_min g) holds
p is_a_fixpoint_of g
let g be monotone Function of P,P; :: thesis: ( g is continuous & p = sup (iter_min g) implies p is_a_fixpoint_of g )
A01: dom g = the carrier of P by FUNCT_2:def 1;
reconsider L = g .: (iter_min g) as non empty Chain of P by ThChain1;
assume A1: ( g is continuous & p = sup (iter_min g) ) ; :: thesis: p is_a_fixpoint_of g
then g . p = sup L by Thcontinuous01
.= p by A1, ThiterSet2 ;
hence p is_a_fixpoint_of g by A01, ABIAN:def 3; :: thesis: verum