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

now

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

end;

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