theorem Th3: :: ZF_LANG1:3

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