for A being QC-alphabet
for F, G, H being Element of QC-WFF A holds { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G) : ( t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H ) } c= F -entry_points_in_subformula_tree_of H