:: deftheorem defines conjunctive GRZLOG_1:def 19 :
for t being GRZ-formula holds
( t is conjunctive iff Polish-WFF-head t = '&' );