let G be addGroup; :: thesis: for a, b being Element of G st a in con_class b holds
b in con_class a
let a, b be Element 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 Th81;
hence b in con_class a by Th81; :: thesis: verum