:: deftheorem Def1 defines proper GROUP_22:def 1 :
for G being Group
for IT being Subgroup of G holds
( IT is proper iff multMagma(# the carrier of IT, the multF of IT #) <> multMagma(# the carrier of G, the multF of G #) );