let
G
be
Group
;
:: thesis:
for
a
,
b
being
Element
of
G
holds
[.
a
,
a
,
b
.]
=
1_
G
let
a
,
b
be
Element
of
G
;
:: thesis:
[.
a
,
a
,
b
.]
=
1_
G
thus
[.
a
,
a
,
b
.]
=
[.
(
1_
G
)
,
b
.]
by
Th20
.=
1_
G
by
Th19
;
:: thesis:
verum