let G be addGroup; :: thesis: for g being Element of G
for H being strict Subgroup of G holds H * g in con_class H
let g be Element of G; :: thesis: for H being strict Subgroup of G holds H * g in con_class H
let H be strict Subgroup of G; :: thesis: H * g in con_class H
H,H * g are_conjugated by Th102;
hence H * g in con_class H by Def12; :: thesis: verum