reconsider H' = (1). H as GroupWithOperators of O ;
reconsider H' = H' as StableSubgroup of H ;
take H' ; :: thesis: H' is normal

now

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

end;

hence H' is normal by Def10; :: thesis: verum