Subformulae VERUM = root-tree VERUM by Def9;