let
G
be
Group
;
:: thesis:
for
a
,
b
being
Element
of
G
holds
[.
a
,
b
.]
=
(
(
b
*
a
)
"
)
*
(
a
*
b
)
let
a
,
b
be
Element
of
G
;
:: thesis:
[.
a
,
b
.]
=
(
(
b
*
a
)
"
)
*
(
a
*
b
)
thus
[.
a
,
b
.]
=
(
(
a
"
)
*
(
b
"
)
)
*
(
a
*
b
)
by
Th16
.=
(
(
b
*
a
)
"
)
*
(
a
*
b
)
by
GROUP_1:17
;
:: thesis:
verum