let W be Universe; :: thesis: ( omega in W implies 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 ) )

assume A1: omega in W ; :: thesis: 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 )

then consider a being Ordinal of W, M being non empty set such that

A2: ( a is_cofinal_with omega & M = Rank a & M <==> W ) by Th39;

take a ; :: thesis: ex M being non empty set st

( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF )

take M ; :: thesis: ( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF )

W is being_a_model_of_ZF by A1, ZF_REFLE:6;

hence ( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF ) by A2, Th10; :: thesis: verum

( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF ) )

assume A1: omega in W ; :: thesis: 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 )

then consider a being Ordinal of W, M being non empty set such that

A2: ( a is_cofinal_with omega & M = Rank a & M <==> W ) by Th39;

take a ; :: thesis: ex M being non empty set st

( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF )

take M ; :: thesis: ( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF )

W is being_a_model_of_ZF by A1, ZF_REFLE:6;

hence ( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF ) by A2, Th10; :: thesis: verum