let F be Element of QC-WFF ; :: thesis: for t', t being Element of dom (tree_of_subformulae F) st t' in succ t holds
(tree_of_subformulae F) . t' is_immediate_constituent_of (tree_of_subformulae F) . t
let t', t be Element of dom (tree_of_subformulae F); :: thesis: ( t' in succ t implies (tree_of_subformulae F) . t' is_immediate_constituent_of (tree_of_subformulae F) . t )
assume t' in succ t ; :: thesis: (tree_of_subformulae F) . t' is_immediate_constituent_of (tree_of_subformulae F) . t
then ex n being Element of NAT st
( t' = t ^ <*n*> & t ^ <*n*> in dom (tree_of_subformulae F) ) ;
hence (tree_of_subformulae F) . t' is_immediate_constituent_of (tree_of_subformulae F) . t by Th36; :: thesis: verum