theorem Th90: :: GRZLOG_1:34
for t being GRZ-formula st LD-EqClassOf t is LD-provable holds
t is LD-provable