theorem :: ZFREFLE1:40

for W being Universe st omega in W holds
ex a being Ordinal of W ex M being non empty set st
( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF )