:: deftheorem defines GRZ-axiomatic GRZLOG_1:def 34 :
for t being GRZ-formula holds
( t is GRZ-axiomatic iff t in GRZ-axioms );