for A being QC-alphabet
for F, G, H being Element of QC-WFF A st ( H is_immediate_constituent_of G or H is_proper_subformula_of G or H is_subformula_of G ) & G in Subformulae F holds
H in Subformulae F