for A being QC-alphabet
for F being Element of QC-WFF A holds rng (tree_of_subformulae F) = Subformulae F