let F be Element of QC-WFF ; :: thesis: for G2, G1 being Subformula of F st G2 is_subformula_of G1 holds
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
let G2, G1 be Subformula of F; :: thesis: ( G2 is_subformula_of G1 implies 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 )
assume A1: G2 is_subformula_of G1 ; :: thesis: 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

now

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

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: verum