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