let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A holds index ('not' p) = index p
let p be Element of CQC-WFF A; :: thesis: index ('not' p) = index p
still_not-bound_in p = still_not-bound_in ('not' p) by QC_LANG3:7;
hence index ('not' p) = index p ; :: thesis: verum