let G be addGroup; :: 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