theorem Th156: :: ZF_LANG1:156

for F, H being ZF-formula
for x, y being Variable holds
( 'not' F = ('not' H) / (x,y) iff F = H / (x,y) )