for A being QC-alphabet
for F being Element of QC-WFF A holds not F is_proper_subformula_of VERUM A