theorem Th8: :: QC_LANG4:8

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_immediate_constituent_of G holds
H in rng (tree_of_subformulae F)