for A being QC-alphabet
for F being Element of QC-WFF A
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