set IT = sup (iter_min g);
take sup (iter_min g) ; :: thesis: ( sup (iter_min g) is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
sup (iter_min g) <= p ) )
thus ( sup (iter_min g) is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
sup (iter_min g) <= p ) ) by A1, Lm8, Lm9; :: thesis: verum