let G be addGroup; :: thesis: for A, B being Subset of G holds
( A in con_class B iff A,B are_conjugated )
let A, B be Subset 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 Subset of G st
( A = C & B,C are_conjugated ) ;
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 ; :: thesis: verum