set H = (1). G;
set H9 = (1). G;
reconsider H = (1). G as StableSubgroup of G ;
take (1). G ; :: thesis: ( (1). G is strict & (1). G is normal )

now :: thesis: for H99 being strict Subgroup of G st H99 = multMagma(# the carrier of H, the multF of H #) holds
H99 is normal

reconsider G9 = G as Group ;
let H99 be strict Subgroup of G; :: thesis: ( H99 = multMagma(# the carrier of H, the multF of H #) implies H99 is normal )
assume A1: H99 = multMagma(# the carrier of H, the multF of H #) ; :: thesis: H99 is normal
A2: the multF of ((1). G9) = the multF of G9 || the carrier of ((1). G9) by GROUP_2:def 5;
the carrier of ((1). G9) = {(1_ G9)} by GROUP_2:def 7
.= the carrier of ((1). G) by Def8 ;
hence H99 is normal by A1, A2, GROUP_2:def 5; :: thesis: verum

end;

hence ( (1). G is strict & (1). G is normal ) ; :: thesis: verum