let G, F, H be Element of QC-WFF ; :: thesis: ( G in rng (tree_of_subformulae F) & H is_immediate_constituent_of G implies H in rng (tree_of_subformulae F) )
assume A1: ( G in rng (tree_of_subformulae F) & H is_immediate_constituent_of G ) ; :: thesis: H in rng (tree_of_subformulae F)
then consider x being set such that
A2: ( x in dom (tree_of_subformulae F) & G = (tree_of_subformulae F) . x ) by FUNCT_1:def 5;
consider t being Element of dom (tree_of_subformulae F) such that
A3: t = x by A2;
consider n being Element of NAT such that
A4: ( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) by A1, A2, A3, Th36;
thus H in rng (tree_of_subformulae F) by A4, FUNCT_1:def 5; :: thesis: verum