let G be addGroup; for H1, H2 being strict Subgroup of G st H1,H2 are_conjugated holds
H2,H1 are_conjugated
let H1, H2 be strict Subgroup of G; ( H1,H2 are_conjugated implies H2,H1 are_conjugated )
given g being Element of G such that A1:
addMagma(# the carrier of H1, the addF of H1 #) = H2 * g
; GROUP_1A:def 39 H2,H1 are_conjugated
H2 = H1 * (- g)
by A1, ThB62;
hence
H2,H1 are_conjugated
; verum