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