let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A
for G1, G2 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 F be Element of QC-WFF A; :: thesis: for G1, G2 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 G1, G2 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 )
consider t9 being FinSequence such that
A1: t9 = t1 ^ s ;
(tree_of_subformulae F) . t1 = G1 by Def5;
then A2: t1 in F -entry_points_in_subformula_tree_of G1 by Def3;
assume t1 ^ s is Entry_Point_in_Subformula_Tree of G2 ; :: thesis: s in G1 -entry_points_in_subformula_tree_of G2
then t9 in { t2 where t2 is Entry_Point_in_Subformula_Tree of G2 : t2 = t2 } by A1;
then t9 in entry_points_in_subformula_tree G2 by Th36;
hence s in G1 -entry_points_in_subformula_tree_of G2 by A2, A1, Th28; :: thesis: verum