let
M
be
MidSp
;
:: thesis:
for
a
,
b
,
c
being
Element
of
M
holds
a
@
(
b
@
c
)
=
(
a
@
b
)
@
(
a
@
c
)
let
a
,
b
,
c
be
Element
of
M
;
:: thesis:
a
@
(
b
@
c
)
=
(
a
@
b
)
@
(
a
@
c
)
a
@
(
b
@
c
)
=
(
a
@
a
)
@
(
b
@
c
)
by
Def3
.=
(
a
@
b
)
@
(
a
@
c
)
by
Def3
;
hence
a
@
(
b
@
c
)
=
(
a
@
b
)
@
(
a
@
c
)
;
:: thesis:
verum