for X being set
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 )