x
is
strict
Subgroup
of
G
by
GROUP_3:def 1
;
hence
x
is
strict
normal
Subgroup
of
G
by
GROUP_3:116
;
:: thesis:
verum