let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A
for G1, G2 being Subformula of F st ex 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 holds
G2 is_subformula_of G1
let F be Element of QC-WFF A; :: thesis: for G1, G2 being Subformula of F st ex 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 holds
G2 is_subformula_of G1
let G1, G2 be Subformula of F; :: thesis: ( ex 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 implies G2 is_subformula_of G1 )
given t1 being Entry_Point_in_Subformula_Tree of G1, t2 being Entry_Point_in_Subformula_Tree of G2 such that A1: t1 is_a_prefix_of t2 ; :: thesis: G2 is_subformula_of G1
( (tree_of_subformulae F) . t1 = G1 & (tree_of_subformulae F) . t2 = G2 ) by Def5;
hence G2 is_subformula_of G1 by A1, Th13; :: thesis: verum