for A being QC-alphabet
for F, G being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) holds
( t in F -entry_points_in_subformula_tree_of G iff (tree_of_subformulae F) | t = tree_of_subformulae G )