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;