for G being Group
for a, g being Element of G holds a |^ g in con_class a by Th80, Th74;