:: deftheorem Def9 defines HP-Subformulae HILBERT2:def 9 :
for b₁ being ManySortedSet of HP-WFF holds
( b₁ = HP-Subformulae iff ( b₁ . VERUM = root-tree VERUM & ( for n being Element of NAT holds b₁ . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p9, q9 being DecoratedTree of HP-WFF st
( p9 = b₁ . p & q9 = b₁ . q & b₁ . (p '&' q) = (p '&' q) -tree (p9,q9) & b₁ . (p => q) = (p => q) -tree (p9,q9) ) ) ) );