theorem Th6: :: QC_LANG4:6

for A being QC-alphabet
for n being Nat
for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) st t ^ <*n*> in dom (tree_of_subformulae F) holds
ex G being Element of QC-WFF A st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t )