let x, y, z be LD-EqClass; :: thesis: x '&' (y 'or' z) = (x '&' y) 'or' (x '&' z)
consider t being GRZ-formula such that
A1: x = LD-EqClassOf t by Th88;
consider u being GRZ-formula such that
A2: y = LD-EqClassOf u by Th88;
consider v being GRZ-formula such that
A3: z = LD-EqClassOf v by Th88;
(t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) is LD-provable ;
then A5: LD-EqClassOf (t '&' (u 'or' v)) = LD-EqClassOf ((t '&' u) 'or' (t '&' v)) by Th80, Def76;
thus x '&' (y 'or' z) = (LD-EqClassOf t) '&' (LD-EqClassOf (u 'or' v)) by A1, A2, A3, Th96
.= LD-EqClassOf ((t '&' u) 'or' (t '&' v)) by A5, Def92
.= (LD-EqClassOf (t '&' u)) 'or' (LD-EqClassOf (t '&' v)) by Th96
.= (LD-EqClassOf (t '&' u)) 'or' ((LD-EqClassOf t) '&' (LD-EqClassOf v)) by Def92
.= (x '&' y) 'or' (x '&' z) by A1, A2, A3, Def92 ; :: thesis: verum