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 & ( 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 Th35;
consider b being Ordinal of W such that
A3: ( a in b & phi . b = b ) by A1, A2, Th30;
reconsider M = Rank b as non empty set by A3, CLASSES1:42;
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 A2, A3; :: thesis: verum