theorem Th16: :: QC_LANG4:16

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 t is_a_proper_prefix_of t9 holds
(tree_of_subformulae F) . t9 is_proper_subformula_of (tree_of_subformulae F) . t