:: deftheorem defines GRZ-provable GRZLOG_1:def 35 :
for t being GRZ-formula holds
( t is GRZ-provable iff GRZ-axioms , GRZ-rules |- t );