let
M
be
MidSp
;
:: thesis:
for
a
,
b
being
Element
of
M
holds
[
a
,
(
a
@
b
)
]
##
[
(
a
@
b
)
,
b
]
let
a
,
b
be
Element
of
M
;
:: thesis:
[
a
,
(
a
@
b
)
]
##
[
(
a
@
b
)
,
b
]
a
@
b
=
(
a
@
b
)
@
(
a
@
b
)
by
Def3
;
then
a
,
a
@
b
@@
a
@
b
,
b
;
hence
[
a
,
(
a
@
b
)
]
##
[
(
a
@
b
)
,
b
]
;
:: thesis:
verum