G is_subformula_of F by Def4;
hence F -entry_points_in_subformula_tree_of G is non empty AntiChain_of_Prefixes of dom (tree_of_subformulae F) by Th50; :: thesis: verum