let G be addGroup; :: thesis: for h being Element of G holds
( 2 * h = 0_ G iff - h = h )
let h be Element of G; :: thesis: ( 2 * h = 0_ G iff - h = h )
thus ( 2 * h = 0_ G implies h = - h ) :: thesis: ( - h = h implies 2 * h = 0_ G )
proof
assume 2 * h = 0_ G ; :: thesis: h = - h
then h + h = 0_ G by Th26;
hence h = - h by Th11; :: thesis: verum
end;
assume h = - h ; :: thesis: 2 * h = 0_ G
hence 2 * h = h + (- h) by Th26
.= 0_ G by Def5 ;
:: thesis: verum