for M being non empty set st M is being_a_model_of_ZF holds
M |= ZF-axioms