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 Element of dom (tree_of_subformulae G1) st s in G1 -entry_points_in_subformula_tree_of G2 holds
t1 ^ s is Entry_Point_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 Element of dom (tree_of_subformulae G1) st s in G1 -entry_points_in_subformula_tree_of G2 holds
t1 ^ s is Entry_Point_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 Element of dom (tree_of_subformulae G1) st s in G1 -entry_points_in_subformula_tree_of G2 holds
t1 ^ s is Entry_Point_in_Subformula_Tree of G2
let t1 be Entry_Point_in_Subformula_Tree of G1; :: thesis: for s being Element of dom (tree_of_subformulae G1) st s in G1 -entry_points_in_subformula_tree_of G2 holds
t1 ^ s is Entry_Point_in_Subformula_Tree of G2
let s be Element of dom (tree_of_subformulae G1); :: thesis: ( s in G1 -entry_points_in_subformula_tree_of G2 implies t1 ^ s is Entry_Point_in_Subformula_Tree of G2 )
(tree_of_subformulae F) . t1 = G1 by Def5;
then A1: t1 in F -entry_points_in_subformula_tree_of G1 by Def3;
assume s in G1 -entry_points_in_subformula_tree_of G2 ; :: thesis: t1 ^ s is Entry_Point_in_Subformula_Tree of G2
then A2: t1 ^ s in F -entry_points_in_subformula_tree_of G2 by A1, Th27;
F -entry_points_in_subformula_tree_of G2 c= dom (tree_of_subformulae F) by TREES_1:def 11;
then reconsider t9 = t1 ^ s as Element of dom (tree_of_subformulae F) by A2;
(tree_of_subformulae F) . t9 = G2 by A2, Def3;
hence t1 ^ s is Entry_Point_in_Subformula_Tree of G2 by Def5; :: thesis: verum