theorem Th9: :: QC_LANG4:9

for A being QC-alphabet
for F, G, H being Element of QC-WFF A st G in rng (tree_of_subformulae F) & H is_subformula_of G holds
H in rng (tree_of_subformulae F)