theorem :: ZF_LANG1:86

for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is negative holds
( M,v |= H iff not M,v |= the_argument_of H )