theorem Th119: :: GROUP_2:119

for G being Group
for a being Element of G
for H being Subgroup of G holds
( a in H iff H * a = carr H )