theorem Th75: :: GRZLOG_1:28

for t being GRZ-formula holds t '=' t is LD-provable