theorem Th28: :: GROUP_9:28

for O being set
for G being GroupWithOperators of O
for N1, N2 being strict normal StableSubgroup of G holds N1 * N2 = N2 * N1