reconsider H9 = (1). H as GroupWithOperators of O ;

reconsider H9 = H9 as StableSubgroup of H ;

take H9 ; :: thesis: H9 is normal

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

hence
H9 is normal
; :: thesis: verumH99 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;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