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