:: deftheorem Def13 defines simple GROUP_9:def 13 :
for O being set
for IT being GroupWithOperators of O holds
( IT is simple iff ( not IT is trivial & ( for H being strict normal StableSubgroup of IT holds
( not H <> (Omega). IT or not H <> (1). IT ) ) ) );