theorem Th90: :: GRZLOG_1:34

for t being GRZ-formula st LD-EqClassOf t is LD-provable holds
t is LD-provable