theorem :: GRZLOG_1:43

for x, y being LD-EqClass holds
( x => y is LD-provable iff x = x '&' y ) by Th92;