theorem Th27: :: QC_LANG4:27

for A being QC-alphabet
for F, G, H being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F)
for s being Element of dom (tree_of_subformulae G) st t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H holds
t ^ s in F -entry_points_in_subformula_tree_of H