theorem :: HILBERT2:31

for n being Element of NAT holds Subformulae (prop n) = root-tree (prop n) by Def9;