theorem :: QC_LANG3:55
for A being QC-alphabet
for p being Element of QC-WFF A holds Free ('not' p) = Free p by Th39;