theorem Th60: :: ZF_LANG1:60

for p being ZF-formula holds Free ('not' p) = Free p