theorem :: QC_LANG2:62

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_immediate_constituent_of G ) by Th53, Th59;