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