let F be AbGroup; :: thesis: for a being Element of F ex b being Element of F st
( a + b = 0. F & b + a = 0. F )
let a be Element of F; :: thesis: ex b being Element of F st
( a + b = 0. F & b + a = 0. F )
consider b being Element of F such that
A1: a + b = 0. F by ALGSTR_0:def 11;
take b ; :: thesis: ( a + b = 0. F & b + a = 0. F )
thus a + b = 0. F by A1; :: thesis: b + a = 0. F
thus b + a = 0. F by A1; :: thesis: verum