theorem Th92: :: GRZLOG_1:36

for x, y being LD-EqClass holds
( x '=' y is LD-provable iff x = y )