let p be Element of CQC-WFF ; :: 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