theorem Th1: :: GRZLOG_1:1

( 'not' <> '&' & 'not' <> '=' & '&' <> '=' )