theorem Th28: :: HILBERT2:28

for p, q being Element of HP-WFF holds
( p => q <> p & p => q <> q )