theorem :: GRZLOG_1:5

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