for A being QC-alphabet
for F being Element of QC-WFF A
for G being Subformula of F holds entry_points_in_subformula_tree G = { t where t is Entry_Point_in_Subformula_Tree of G : t = t }