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