theorem Th26: :: HILBERT2:26

for n being Element of NAT
for p, q being Element of HP-WFF holds p => q <> prop n