let G be Group; :: thesis: for a, g being Element of G holds a |^ g in con_class a
let a, g be Element of G; :: thesis: a |^ g in con_class a
a,a |^ g are_conjugated by Th88;
hence a |^ g in con_class a by Th95; :: thesis: verum