theorem :: HILBERT1:18

for p, q being Element of HP-WFF holds (q => p) => (p => p) in HP_TAUT by Th14, Th15;