theorem Th25: :: QC_LANG4:25

for A being QC-alphabet
for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . t is conjunctive holds
( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_left_argument_of ((tree_of_subformulae F) . t) & t ^ <*1*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*1*>) = the_right_argument_of ((tree_of_subformulae F) . t) )