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