let x, y be LD-EqClass; :: thesis: ( x is LD-provable implies x 'or' y is LD-provable )
assume A1: x is LD-provable ; :: thesis: x 'or' y is LD-provable
consider u being GRZ-formula such that
A2: y = LD-EqClassOf u by Th88;
LD-EqClassOf ('not' (u '&' ('not' u))) = 'not' (LD-EqClassOf (u '&' ('not' u))) by Def91
.= 'not' ((LD-EqClassOf u) '&' (LD-EqClassOf ('not' u))) by Def92
.= 'not' (y '&' ('not' y)) by A2, Def91 ;
then A5: x '&' (('not' y) 'or' y) is LD-provable by A1, Th91;
x '&' (('not' y) 'or' y) = (x '&' ('not' y)) 'or' (x '&' y) by Th104
.= ((x '&' ('not' y)) 'or' x) '&' ((x '&' ('not' y)) 'or' y) by Th105 ;
then A6: (x '&' ('not' y)) 'or' y is LD-provable by A5, Th91;
(x '&' ('not' y)) 'or' y = (y 'or' x) '&' (y 'or' ('not' y)) by Th105;
hence x 'or' y is LD-provable by A6, Th91; :: thesis: verum