let G be addGroup; :: thesis: for H1, H2 being strict Subgroup of G holds
( H1 in con_class H2 iff H1,H2 are_conjugated )
let H1, H2 be strict Subgroup of G; :: thesis: ( H1 in con_class H2 iff H1,H2 are_conjugated )
thus ( H1 in con_class H2 implies H1,H2 are_conjugated ) :: thesis: ( H1,H2 are_conjugated implies H1 in con_class H2 )

proof

assume H1 in con_class H2 ; :: thesis: H1,H2 are_conjugated
then ex H3 being strict Subgroup of G st
( H1 = H3 & H2,H3 are_conjugated ) by Def12;
hence H1,H2 are_conjugated ; :: thesis: verum

end;

assume H1,H2 are_conjugated ; :: thesis: H1 in con_class H2
hence H1 in con_class H2 by Def12; :: thesis: verum