theorem Th25: :: HILBERT2:25

for p, q being Element of HP-WFF holds p => q <> VERUM