let
G
be
Group
;
:: thesis:
for
H
being
strict
Subgroup
of
G
holds
H
/\
H
=
H
let
H
be
strict
Subgroup
of
G
;
:: thesis:
H
/\
H
=
H
the
carrier
of
(
H
/\
H
)
=
(
carr
H
)
/\
(
carr
H
)
by
Def10
.= the
carrier
of
H
;
hence
H
/\
H
=
H
by
Th59
;
:: thesis:
verum