theorem :: HILBERT1:16

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