let p be QC-formula; :: thesis: still_not-bound_in ('not' p) = still_not-bound_in p
A1: 'not' p is negative by QC_LANG1:def 17;
then the_argument_of ('not' p) = p by QC_LANG1:def 22;
hence still_not-bound_in ('not' p) = still_not-bound_in p by A1, Th10; :: thesis: verum