theorem Th4: :: GRZLOG_1:2

( GRZ-arity . 'not' = 1 & GRZ-arity . '&' = 2 & GRZ-arity . '=' = 2 )