let G be Group; :: thesis: for a being Element of G st ( a, 1_ G are_conjugated or 1_ G,a are_conjugated ) holds
a = 1_ G
let a be Element of G; :: thesis: ( ( a, 1_ G are_conjugated or 1_ G,a are_conjugated ) implies a = 1_ G )
assume A1: ( a, 1_ G are_conjugated or 1_ G,a are_conjugated ) ; :: thesis: a = 1_ G

now :: thesis: a = 1_ G

per cases ( a, 1_ G are_conjugated or 1_ G,a are_conjugated ) by A1;

suppose a, 1_ G are_conjugated ; :: thesis: a = 1_ G

then ex g being Element of G st 1_ G = a |^ g by Th74;
hence a = 1_ G by Th18; :: thesis: verum

end;

suppose 1_ G,a are_conjugated ; :: thesis: a = 1_ G

then ex g being Element of G st 1_ G = a |^ g ;
hence a = 1_ G by Th18; :: thesis: verum

end;

end;

end;

hence a = 1_ G ; :: thesis: verum