theorem :: GRZLOG_1:50

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