for t being GRZ-formula holds
( t is negative iff ex u being GRZ-formula st t = 'not' u )