:: deftheorem defines simple GROUP_9:def 12 :
for IT being Group holds
( IT is simple iff ( not IT is trivial & ( for H being strict normal Subgroup of IT holds
( not H <> (Omega). IT or not H <> (1). IT ) ) ) );