theorem :: QC_LANG2:60

for A being QC-alphabet
for G, H being Element of QC-WFF A holds
( not G is_proper_subformula_of H or not H is_proper_subformula_of G ) by Th59;