let G be addGroup; :: thesis: for H1, H2 being strict Subgroup of G st H1 in con_class H2 holds
H2 in con_class H1
let H1, H2 be strict Subgroup of G; :: thesis: ( H1 in con_class H2 implies H2 in con_class H1 )
assume H1 in con_class H2 ; :: thesis: H2 in con_class H1
then H1,H2 are_conjugated by Th107;
hence H2 in con_class H1 by Th107; :: thesis: verum