theorem :: QC_LANG4:17

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 = F iff t = {} )