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