for G being Group
for g being Element of G
for H being strict Subgroup of G holds H |^ g in con_class H