for A being QC-alphabet
for p being Element of QC-WFF A holds Fixed ('not' p) = Fixed p by Th39;