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

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

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

end;

hence H9 is normal ; :: thesis: verum