let
G
be
Group
;
:: thesis:
for
H
being
Subgroup
of
G
holds
(1).
H
=
(1).
G
let
H
be
Subgroup
of
G
;
:: thesis:
(1).
H
=
(1).
G
A1
:
1_
H
=
1_
G
by
Th44
;
(
(1).
H
is
Subgroup
of
G
& the
carrier
of
(
(1).
H
)
=
{
(
1_
H
)
}
)
by
Def7
,
Th56
;
hence
(1).
H
=
(1).
G
by
A1
,
Def7
;
:: thesis:
verum