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