for A being QC-alphabet
for F, G being Element of QC-WFF A holds
( G in rng (tree_of_subformulae F) iff G is_subformula_of F )