reconsider
H
=
multMagma
(# the
carrier
of
N
, the
multF
of
N
#) as
strict
normal
Subgroup
of
G
by
Lm6
;
Cosets
N
=
Cosets
H
by
Def14
;
hence
not
G
./.
N
is
empty
;
:: thesis:
verum