:: deftheorem Def2 defines tree_of_subformulae QC_LANG4:def 2 :
for A being QC-alphabet
for p being Element of QC-WFF A
for b₃ being finite DecoratedTree of QC-WFF A holds
( b₃ = tree_of_subformulae p iff ( b₃ . {} = p & ( for x being Element of dom b₃ holds succ (b₃,x) = list_of_immediate_constituents (b₃ . x) ) ) );