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