let G be Group; :: thesis: for a, b being Element of G holds
( a in con_class b iff a,b are_conjugated )
let a, b be Element of G; :: thesis: ( a in con_class b iff a,b are_conjugated )
thus ( a in con_class b implies a,b are_conjugated ) :: thesis: ( a,b are_conjugated implies a in con_class b )

proof

assume a in con_class b ; :: thesis: a,b are_conjugated
then ex c being Element of G st
( a = c & b,c are_conjugated ) by Th80;
hence a,b are_conjugated ; :: thesis: verum

end;

assume a,b are_conjugated ; :: thesis: a in con_class b
hence a in con_class b by Th80; :: thesis: verum