let X be set ; :: thesis: for W being Universe st omega in W & X in W holds
ex M being non empty set st
( X in M & M in W & M is being_a_model_of_ZF )

let W be Universe; :: thesis: ( omega in W & X in W implies ex M being non empty set st
( X in M & M in W & M is being_a_model_of_ZF ) )

assume A1: omega in W ; :: thesis: ( not X in W or ex M being non empty set st
( X in M & M in W & M is being_a_model_of_ZF ) )

A2: W = Rank (On W) by CLASSES2:50;
assume X in W ; :: thesis: ex M being non empty set st
( X in M & M in W & M is being_a_model_of_ZF )

then the_rank_of X in the_rank_of W by CLASSES1:68;
then the_rank_of X in On W by ;
then reconsider a = the_rank_of X as Ordinal of W by ZF_REFLE:7;
consider b being Ordinal of W, M being non empty set such that
A3: a in b and
A4: M = Rank b and
A5: M <==> W by ;
take M ; :: thesis: ( X in M & M in W & M is being_a_model_of_ZF )
X c= Rank a by CLASSES1:def 9;
then A6: X in Rank (succ a) by CLASSES1:32;
succ a c= b by ;
then Rank (succ a) c= M by ;
hence X in M by A6; :: thesis: ( M in W & M is being_a_model_of_ZF )
b in On W by ZF_REFLE:7;
hence M in W by ; :: thesis:
W is being_a_model_of_ZF by ;
then W |= ZF-axioms by Th4;
then M |= ZF-axioms by ;
hence M is being_a_model_of_ZF by ; :: thesis: verum