theorem Th94: :: ZF_LANG1:94

for H being ZF-formula
for x being Variable
for M being non empty set st M |= H holds
M |= Ex (x,H)