:: deftheorem Def3 defines -entry_points_in_subformula_tree_of QC_LANG4:def 3 :
for A being QC-alphabet
for F, G being Element of QC-WFF A
for b₄ being AntiChain_of_Prefixes of dom (tree_of_subformulae F) holds
( b₄ = F -entry_points_in_subformula_tree_of G iff for t being Element of dom (tree_of_subformulae F) holds
( t in b₄ iff (tree_of_subformulae F) . t = G ) );