:: deftheorem Def5 defines Entry_Point_in_Subformula_Tree QC_LANG4:def 5 :
for A being QC-alphabet
for F being Element of QC-WFF A
for G being Subformula of F
for b₄ being Element of dom (tree_of_subformulae F) holds
( b₄ is Entry_Point_in_Subformula_Tree of G iff (tree_of_subformulae F) . b₄ = G );