theorem :: GRZLOG_1:8

for t being GRZ-formula holds
( t is atomic or t is negative or t is conjunctive or t is being_equality )