theorem Th114: :: GROUP_1A:313
for G being addGroup holds
( (0). G is normal & (Omega). G is normal ) by Th67, Th69;