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