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