let
G
be
Group
;
:: thesis:
for
H1
,
H2
being
Subgroup
of
G
holds
1_
H1
=
1_
H2
let
H1
,
H2
be
Subgroup
of
G
;
:: thesis:
1_
H1
=
1_
H2
thus
1_
H1
=
1_
G
by
Th44
.=
1_
H2
by
Th44
;
:: thesis:
verum