theorem Th30: :: HILBERT2:30

Subformulae VERUM = root-tree VERUM by Def9;