let
G
be
Group
;
:: thesis:
for
H
being
Subgroup
of
G
holds
(1).
G
is
Subgroup
of
H
let
H
be
Subgroup
of
G
;
:: thesis:
(1).
G
is
Subgroup
of
H
(1).
G
=
(1).
H
by
Th63
;
hence
(1).
G
is
Subgroup
of
H
;
:: thesis:
verum