theorem Th30: :: QC_LANG4:30

for A being QC-alphabet
for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) holds (tree_of_subformulae F) | t = tree_of_subformulae ((tree_of_subformulae F) . t)