for p, q being Element of HP-WFF st q in HP_TAUT holds
p => q in HP_TAUT