let A be QC-alphabet ; :: thesis:
let F be Element of QC-WFF A; :: thesis:
let G1, G2 be Subformula of F; :: thesis:
assume A1: G2 is_subformula_of G1 ; :: thesis:

let t1 be Entry_Point_in_Subformula_Tree of G1; :: thesis:
consider H being Element of QC-WFF A such that
A2: H = G2 ;
reconsider H = H as Subformula of G1 by A1, A2, Def4;
set s = the Entry_Point_in_Subformula_Tree of H;
(tree_of_subformulae G1) . the Entry_Point_in_Subformula_Tree of H = H by Def5;
then the Entry_Point_in_Subformula_Tree of H in G1 -entry_points_in_subformula_tree_of G2 by A2, Def3;
then t1 ^ the Entry_Point_in_Subformula_Tree of H is Entry_Point_in_Subformula_Tree of G2 by Th37;
then consider t2 being Entry_Point_in_Subformula_Tree of G2 such that
A3: t2 = t1 ^ the Entry_Point_in_Subformula_Tree of H ;
take t2 = t2; :: thesis:
thus t1 is_a_prefix_of t2 by A3, TREES_1:1; :: thesis:

end;

hence for 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 ; :: thesis: