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 is_elementary_subsystem_of 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 is_elementary_subsystem_of W ) )

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

( a in b & M = Rank b & 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: a in b and

A5: phi . b = b by A1, A2, Th28;

reconsider M = Rank b as non empty set by A4, CLASSES1:36;

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

( a in b & M = Rank b & M is_elementary_subsystem_of W )

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

thus ( a in b & M = Rank b & M is_elementary_subsystem_of W ) by A3, A4, A5; :: thesis: verum

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

( a in b & M = Rank b & M is_elementary_subsystem_of 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 is_elementary_subsystem_of W ) )

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

( a in b & M = Rank b & 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: a in b and

A5: phi . b = b by A1, A2, Th28;

reconsider M = Rank b as non empty set by A4, CLASSES1:36;

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

( a in b & M = Rank b & M is_elementary_subsystem_of W )

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

thus ( a in b & M = Rank b & M is_elementary_subsystem_of W ) by A3, A4, A5; :: thesis: verum