let G be addGroup; :: thesis: for A, B being Subset of G st A in con_class B holds
B in con_class A
let A, B be Subset of G; :: thesis: ( A in con_class B implies B in con_class A )
assume A in con_class B ; :: thesis: B in con_class A
then A,B are_conjugated by Th95;
hence B in con_class A ; :: thesis: verum