let
G
be
Group
;
:: thesis:
for
N
,
H
being
Subgroup
of
G
holds
N
`
H
c=
N
~
H
let
N
,
H
be
Subgroup
of
G
;
:: thesis:
N
`
H
c=
N
~
H
A1
:
N
`
H
c=
carr
H
by
Th53
;
carr
H
c=
N
~
H
by
Th54
;
hence
N
`
H
c=
N
~
H
by
A1
;
:: thesis:
verum