let A be QC-alphabet ; :: thesis: for F, G, H being Element of QC-WFF A st G in rng (tree_of_subformulae F) & H is_immediate_constituent_of G holds
H in rng (tree_of_subformulae F)
let F, G, H be Element of QC-WFF A; :: thesis: ( G in rng (tree_of_subformulae F) & H is_immediate_constituent_of G implies H in rng (tree_of_subformulae F) )
assume that
A1: G in rng (tree_of_subformulae F) and
A2: H is_immediate_constituent_of G ; :: thesis: H in rng (tree_of_subformulae F)
consider x being object such that
A3: x in dom (tree_of_subformulae F) and
A4: G = (tree_of_subformulae F) . x by A1, FUNCT_1:def 3;
consider t being Element of dom (tree_of_subformulae F) such that
A5: t = x by A3;
ex n being Nat st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) by A2, A4, A5, Th7;
hence H in rng (tree_of_subformulae F) by FUNCT_1:def 3; :: thesis: verum