for G being Group
for A being Subgroup of G
for a being Element of G
for X being Subgroup of A
for x being Element of A st x = a holds
( x * X = a * X & X * x = X * a )