theorem Th91: :: GRZLOG_1:35

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