let W be Universe; :: thesis: for a being Ordinal of st omega in W holds
ex b being Ordinal of ex M being non empty set st
( a in b & M = Rank b & M <==> W )
let a be Ordinal of ; :: thesis: ( omega in W implies ex b being Ordinal of 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 ex M being non empty set st
( a in b & M = Rank b & M <==> W )
then consider b being Ordinal of , M being non empty set such that
A1: ( a in b & M = Rank b & M is_elementary_subsystem_of W ) by Th36;
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