let p be ZF-formula; :: thesis: the_argument_of ('not' p) = p
'not' p is negative ;
hence the_argument_of ('not' p) = p by ZF_LANG:def 30; :: thesis: verum