let
G
be
strict
Group
;
:: thesis:
for
a
,
b
being
Element
of
G
holds
[.
a
,
b
.]
in
G
`
let
a
,
b
be
Element
of
G
;
:: thesis:
[.
a
,
b
.]
in
G
`
(
a
in
(Omega).
G
&
b
in
(Omega).
G
)
by
STRUCT_0:def 5
;
hence
[.
a
,
b
.]
in
G
`
by
Th65
;
:: thesis:
verum