:: deftheorem defines LD-provable GRZLOG_1:def 42 :
for x being LD-EqClass holds
( x is LD-provable iff ex t being GRZ-formula st
( x = LD-EqClassOf t & t is LD-provable ) );