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 t9 in succ t holds
(tree_of_subformulae F) . t9 is_immediate_constituent_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 t9 in succ t holds
(tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t
let t, t9 be Element of dom (tree_of_subformulae F); :: thesis: ( t9 in succ t implies (tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t )
assume t9 in succ t ; :: thesis: (tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t
then ex n being Nat st
( t9 = t ^ <*n*> & t ^ <*n*> in dom (tree_of_subformulae F) ) ;
hence (tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t by Th7; :: thesis: verum