let F be Element of QC-WFF ; :: thesis: for G being Subformula of F
for t being Entry_Point_in_Subformula_Tree of G holds t in entry_points_in_subformula_tree G
let G be Subformula of F; :: thesis: for t being Entry_Point_in_Subformula_Tree of G holds t in entry_points_in_subformula_tree G
let t be Entry_Point_in_Subformula_Tree of G; :: thesis: t in entry_points_in_subformula_tree G
(tree_of_subformulae F) . t = G by Def5;
hence t in entry_points_in_subformula_tree G by Def3; :: thesis: verum