theorem Th23: :: QC_LANG4:23

for A being QC-alphabet
for m being Nat
for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is universal holds
( (tree_of_subformulae F) . t9 = the_scope_of ((tree_of_subformulae F) . t) & m = 0 )