theorem :: GROUP_1A:309

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