let x, y, z be LD-EqClass; 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
; verum