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_elementary_subsystem_of W ) )
set a = the Ordinal of W;
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_elementary_subsystem_of W )
then consider phi being Ordinal-Sequence of W such that
A2: ( phi is increasing & phi is continuous ) and
A3: for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M is_elementary_subsystem_of W by Th33;
consider b being Ordinal of W such that
A4: the Ordinal of W in b and
A5: ( phi . b = b & b is_cofinal_with omega ) by A1, A2, Th29;
reconsider M = Rank b as non empty set by A4, CLASSES1:36;
take b ; :: thesis: ex M being non empty set st
( b is_cofinal_with omega & M = Rank b & M is_elementary_subsystem_of W )
take M ; :: thesis: ( b is_cofinal_with omega & M = Rank b & M is_elementary_subsystem_of W )
thus ( b is_cofinal_with omega & M = Rank b & M is_elementary_subsystem_of W ) by A3, A4, A5; :: thesis: verum