let F, G be Element of QC-WFF ; :: thesis: for t being Element of dom (tree_of_subformulae F) holds
( t in F -entry_points_in_subformula_tree_of G iff (tree_of_subformulae F) | t = tree_of_subformulae G )
let t be Element of dom (tree_of_subformulae F); :: thesis: ( t in F -entry_points_in_subformula_tree_of G iff (tree_of_subformulae F) | t = tree_of_subformulae G )

now

assume t in F -entry_points_in_subformula_tree_of G ; :: thesis: (tree_of_subformulae F) | t = tree_of_subformulae G
then (tree_of_subformulae F) . t = G by Def3;
hence (tree_of_subformulae F) | t = tree_of_subformulae G by Th60; :: thesis: verum

end;

hence ( t in F -entry_points_in_subformula_tree_of G implies (tree_of_subformulae F) | t = tree_of_subformulae G ) ; :: thesis: ( (tree_of_subformulae F) | t = tree_of_subformulae G implies t in F -entry_points_in_subformula_tree_of G )

now

assume (tree_of_subformulae F) | t = tree_of_subformulae G ; :: thesis: t in F -entry_points_in_subformula_tree_of G
then A1: (tree_of_subformulae F) . t = (tree_of_subformulae G) . {} by TREES_9:35;
(tree_of_subformulae G) . {} = G by Def2;
hence t in F -entry_points_in_subformula_tree_of G by A1, Def3; :: thesis: verum

end;

hence ( (tree_of_subformulae F) | t = tree_of_subformulae G implies t in F -entry_points_in_subformula_tree_of G ) ; :: thesis: verum