theorem :: QC_LANG4:41

for A being QC-alphabet
for F being Element of QC-WFF A
for G1, G2 being Subformula of F st ex t1 being Entry_Point_in_Subformula_Tree of G1 ex t2 being Entry_Point_in_Subformula_Tree of G2 st t1 is_a_prefix_of t2 holds
G2 is_subformula_of G1