theorem :: QC_LANG4:12

for A being QC-alphabet
for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t9 in succ t holds
(tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t