for b being Ordinal
for W being Universe
for phi being normal Ordinal-Sequence of W st omega in W & b in W holds
ex a being Ordinal st
( b in a & a is_a_fixpoint_of phi )