theorem Th11: :: GROUP_1:12

for G being Group
for g, h being Element of G st h * g = 1_ G holds
( h = g " & g = h " )