let A be QC-alphabet ; :: thesis: 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
let F, G, H be Element of QC-WFF A; :: 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 that
A1: ( H is_immediate_constituent_of G or H is_proper_subformula_of G or H is_subformula_of G ) and
A2: G in Subformulae F ; :: thesis: H in Subformulae F
( H is_proper_subformula_of G or H is_subformula_of G ) by A1, Th53;
then A3: H is_subformula_of G ;
G is_subformula_of F by A2, Th82;
then H is_subformula_of F by A3, Th57;
hence H in Subformulae F by Def22; :: thesis: verum