for G being addGroup holds
( (0). G is normal & (Omega). G is normal ) by Th67, Th69;