let W be Universe; :: thesis: for a being Ordinal of W st omega in W holds

ex b being Ordinal of W ex M being non empty set st

( a in b & M = Rank b & M <==> W )

let a be Ordinal of W; :: thesis: ( omega in W implies ex b being Ordinal of W ex M being non empty set st

( a in b & M = Rank b & M <==> W ) )

assume omega in W ; :: thesis: ex b being Ordinal of W ex M being non empty set st

( a in b & M = Rank b & M <==> W )

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

A1: ( a in b & M = Rank b & M is_elementary_subsystem_of W ) by Th34;

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

( a in b & M = Rank b & M <==> W )

take M ; :: thesis: ( a in b & M = Rank b & M <==> W )

thus ( a in b & M = Rank b & M <==> W ) by A1, Th9; :: thesis: verum

ex b being Ordinal of W ex M being non empty set st

( a in b & M = Rank b & M <==> W )

let a be Ordinal of W; :: thesis: ( omega in W implies ex b being Ordinal of W ex M being non empty set st

( a in b & M = Rank b & M <==> W ) )

assume omega in W ; :: thesis: ex b being Ordinal of W ex M being non empty set st

( a in b & M = Rank b & M <==> W )

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

A1: ( a in b & M = Rank b & M is_elementary_subsystem_of W ) by Th34;

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

( a in b & M = Rank b & M <==> W )

take M ; :: thesis: ( a in b & M = Rank b & M <==> W )

thus ( a in b & M = Rank b & M <==> W ) by A1, Th9; :: thesis: verum