:: deftheorem defines @ GROUP_6:def 5 :
for G being Group
for N being normal Subgroup of G
for S being Element of (G ./. N) holds @ S = S;