:: deftheorem defines ./. GROUP_9:def 17 :
for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds G ./. N = HGrWOpStr(# (Cosets N),(CosOp N),(CosAc N) #);