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

now :: thesis: ( G is_subformula_of F implies F -entry_points_in_subformula_tree_of G <> {} )

assume G is_subformula_of F ; :: thesis: F -entry_points_in_subformula_tree_of G <> {}
then G in rng (tree_of_subformulae F) by Th10;
then ex x being object st
( x in dom (tree_of_subformulae F) & G = (tree_of_subformulae F) . x ) by FUNCT_1:def 3;
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 object 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, Th19;
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 3;
hence G is_subformula_of F by Th10; :: thesis: verum