theorem Th28: :: CQC_SIM1:28

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