H is_subformula_of H by Th27;
hence not Subformulae H is empty by Th45; :: thesis: verum