for x, y being LD-EqClass st x is LD-provable holds
x 'or' y is LD-provable