H is_subformula_of H by Th115;
hence not Subformulae H is empty by Th131; :: thesis: verum