let G, F be Element of QC-WFF ; :: thesis: ( G is_subformula_of F iff F -entry_points_in_subformula_tree_of G <> {} )

now

assume G is_subformula_of F ; :: thesis: F -entry_points_in_subformula_tree_of G <> {}
then G in rng (tree_of_subformulae F) by Th39;
then ex x being set st
( x in dom (tree_of_subformulae F) & G = (tree_of_subformulae F) . x ) by FUNCT_1:def 5;
hence F -entry_points_in_subformula_tree_of G <> {} by Def3; :: thesis: verum

end;

hence ( G is_subformula_of F implies F -entry_points_in_subformula_tree_of G <> {} ) ; :: thesis: ( F -entry_points_in_subformula_tree_of G <> {} implies G is_subformula_of F )
assume F -entry_points_in_subformula_tree_of G <> {} ; :: thesis: G is_subformula_of F
then consider x being set such that
A1: x in F -entry_points_in_subformula_tree_of G by XBOOLE_0:def 1;
x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } by A1, Th49;
then ex t being Element of dom (tree_of_subformulae F) st
( x = t & (tree_of_subformulae F) . t = G ) ;
then G in rng (tree_of_subformulae F) by FUNCT_1:def 5;
hence G is_subformula_of F by Th39; :: thesis: verum