theorem :: ZFREFLE1:37

for W being Universe st omega in W holds
ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M <==> W ) )