let F be Element of QC-WFF ; :: thesis: for G2, G1 being Subformula of F
for t1 being Entry_Point_in_Subformula_Tree of G1
for s being FinSequence st t1 ^ s is Entry_Point_in_Subformula_Tree of G2 holds
s in G1 -entry_points_in_subformula_tree_of G2
let G2, G1 be Subformula of F; :: thesis: for t1 being Entry_Point_in_Subformula_Tree of G1
for s being FinSequence st t1 ^ s is Entry_Point_in_Subformula_Tree of G2 holds
s in G1 -entry_points_in_subformula_tree_of G2
let t1 be Entry_Point_in_Subformula_Tree of G1; :: thesis: for s being FinSequence st t1 ^ s is Entry_Point_in_Subformula_Tree of G2 holds
s in G1 -entry_points_in_subformula_tree_of G2
let s be FinSequence; :: thesis: ( t1 ^ s is Entry_Point_in_Subformula_Tree of G2 implies s in G1 -entry_points_in_subformula_tree_of G2 )
assume A1: t1 ^ s is Entry_Point_in_Subformula_Tree of G2 ; :: thesis: s in G1 -entry_points_in_subformula_tree_of G2
(tree_of_subformulae F) . t1 = G1 by Def5;
then A2: t1 in F -entry_points_in_subformula_tree_of G1 by Def3;
consider t' being FinSequence such that
A3: t' = t1 ^ s ;
t' in { t2 where t2 is Entry_Point_in_Subformula_Tree of G2 : t2 = t2 } by A1, A3;
then t' in entry_points_in_subformula_tree G2 by Th68;
hence s in G1 -entry_points_in_subformula_tree_of G2 by A2, A3, Th58; :: thesis: verum