theorem Th14: :: ZF_MODEL:14

for E being non empty set
for f being Function of VAR,E
for H being ZF-formula holds
( E,f |= H iff not E,f |= 'not' H ) by Th4;