let p be ZF-formula; :: thesis: Free ('not' p) = Free p
( 'not' p is negative & the_argument_of ('not' p) = p ) by Th3;
hence Free ('not' p) = Free p by ZF_MODEL:1; :: thesis: verum