theorem Th23: :: CQC_SIM1:23

for A being QC-alphabet
for p being Element of CQC-WFF A holds index ('not' p) = index p