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 )
A1: dom g = the carrier of P by FUNCT_2:def 1;
reconsider L = g .: (iter_min g) as non empty Chain of P by Th1;
assume A2: ( g is continuous & p = sup (iter_min g) ) ; :: thesis: p is_a_fixpoint_of g
then g . p = sup L by Th6
.= p by A2, Th4 ;
hence p is_a_fixpoint_of g by A1, ABIAN:def 3; :: thesis: verum