:: deftheorem defines entry_points_in_subformula_tree QC_LANG4:def 6 :
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 = F -entry_points_in_subformula_tree_of G;