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