let A be QC-alphabet ; :: thesis: for p being QC-formula of A holds still_not-bound_in ('not' p) = still_not-bound_in p
let p be QC-formula of A; :: thesis: still_not-bound_in ('not' p) = still_not-bound_in p
A1: 'not' p is negative ;
then the_argument_of ('not' p) = p by QC_LANG1:def 24;
hence still_not-bound_in ('not' p) = still_not-bound_in p by A1, Th6; :: thesis: verum