for A being QC-alphabet
for F being Element of QC-WFF A holds
( F is_proper_subformula_of FALSUM A iff F is_subformula_of VERUM A ) by Th66;