let
G
be
finite
Group
;
:: thesis:
for
H
being
Subgroup
of
G
holds
index
(
G
,
H
)
>
0
let
H
be
Subgroup
of
G
;
:: thesis:
index
(
G
,
H
)
>
0
card
G
=
(
card
H
)
*
(
index
H
)
by
GROUP_2:147
;
hence
index
(
G
,
H
)
>
0
;
:: thesis:
verum