for G being Group
for a being Element of G holds
( a * ((Omega). G) = the carrier of G & ((Omega). G) * a = the carrier of G )