theorem :: GRZLOG_1:6

for t being GRZ-formula holds
( t is conjunctive iff ex u, v being GRZ-formula st t = u '&' v )