let b be Ordinal; :: thesis: for f being Ordinal-Sequence st b is_a_fixpoint_of f holds
ex a being Ordinal st
( a in dom (criticals f) & b = (criticals f) . a )
let f be Ordinal-Sequence; :: thesis: ( b is_a_fixpoint_of f implies ex a being Ordinal st
( a in dom (criticals f) & b = (criticals f) . a ) )
set X = { a where a is Element of dom f : a is_a_fixpoint_of f } ;
assume A1: b is_a_fixpoint_of f ; :: thesis: ex a being Ordinal st
( a in dom (criticals f) & b = (criticals f) . a )
b in { a where a is Element of dom f : a is_a_fixpoint_of f } by A1;
then b in rng (criticals f) by Th30;
then ex x being object st
( x in dom (criticals f) & b = (criticals f) . x ) by FUNCT_1:def 3;
hence ex a being Ordinal st
( a in dom (criticals f) & b = (criticals f) . a ) ; :: thesis: verum