G is_subformula_of F by Def4;
then G in rng (tree_of_subformulae F) by Th39;
then ex x being set st
( x in dom (tree_of_subformulae F) & (tree_of_subformulae F) . x = G ) by FUNCT_1:def 5;
hence ex b₁ being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . b₁ = G ; :: thesis: verum