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