for F, G, H being ZF-formula 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