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 universal holds
( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_scope_of ((tree_of_subformulae F) . t) )