theorem Th82: :: GROUP_3:82
for G being Group
for a, g being Element of G holds a |^ g in con_class a by Th80, Th74;