let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t9 holds
(tree_of_subformulae F) . t9 is_proper_subformula_of (tree_of_subformulae F) . t
let F be Element of QC-WFF A; :: thesis: for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t9 holds
(tree_of_subformulae F) . t9 is_proper_subformula_of (tree_of_subformulae F) . t
let t, t9 be Element of dom (tree_of_subformulae F); :: thesis: ( t is_a_proper_prefix_of t9 implies (tree_of_subformulae F) . t9 is_proper_subformula_of (tree_of_subformulae F) . t )
set G = (tree_of_subformulae F) . t;
set H = (tree_of_subformulae F) . t9;
assume A1: t is_a_proper_prefix_of t9 ; :: thesis: (tree_of_subformulae F) . t9 is_proper_subformula_of (tree_of_subformulae F) . t
then t is_a_prefix_of t9 ;
then A2: (tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t by Th13;
(tree_of_subformulae F) . t9 <> (tree_of_subformulae F) . t by A1, Th15;
hence (tree_of_subformulae F) . t9 is_proper_subformula_of (tree_of_subformulae F) . t by A2, QC_LANG2:def 21; :: thesis: verum