let H, G, F be ZF-formula; :: thesis: ( ( H is_immediate_constituent_of G or H is_proper_subformula_of G or H is_subformula_of G ) & G in Subformulae F implies H in Subformulae F )
assume A1: ( ( H is_immediate_constituent_of G or H is_proper_subformula_of G or H is_subformula_of G ) & G in Subformulae F ) ; :: thesis: H in Subformulae F
then ( H is_proper_subformula_of G or H is_subformula_of G ) by Th82;
then ( H is_subformula_of G & G is_subformula_of F ) by A1, Def41, Th100;
then H is_subformula_of F by Th86;
hence H in Subformulae F by Def42; :: thesis: verum