let f be Ordinal-Sequence; :: thesis: ( rng (criticals f) = { a where a is Element of dom f : a is_a_fixpoint_of f } & rng (criticals f) c= rng f )
set X = { a where a is Element of dom f : a is_a_fixpoint_of f } ;
On { a where a is Element of dom f : a is_a_fixpoint_of f } = { a where a is Element of dom f : a is_a_fixpoint_of f } by Th28;
hence A1: rng (criticals f) = { a where a is Element of dom f : a is_a_fixpoint_of f } by Th18; :: thesis: rng (criticals f) c= rng f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (criticals f) or x in rng f )
assume x in rng (criticals f) ; :: thesis: x in rng f
then ex a being Element of dom f st
( x = a & a is_a_fixpoint_of f ) by A1;
hence x in rng f by Th27; :: thesis: verum