theorem Th5: :: QC_LANG4:5

for A being QC-alphabet
for F being Element of QC-WFF A holds F in rng (tree_of_subformulae F)