theorem Th27: :: HILBERT2:27

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