let G be Group; :: thesis: for g being Element of G
for A being Subset of G holds A |^ g in con_class A

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