for G being Group
for H1, H2 being strict Subgroup of G st H1 in con_class H2 holds
H2 in con_class H1