for A being QC-alphabet
for F, H being Element of QC-WFF A st 'not' F is_subformula_of H holds
F is_proper_subformula_of H