theorem Th14: :: HILBERT1:14

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