for p being Element of HP-WFF holds p => VERUM in HP_TAUT by Th1, Th15;