let G be non empty right_complementable Fanoian add-associative right_zeroed addLoopStr ; :: thesis: for x being Element of G st x = - x holds
x = 0. G
let x be Element of G; :: thesis: ( x = - x implies x = 0. G )
A1: (- x) + x = 0. G by RLVECT_1:5;
assume x = - x ; :: thesis: x = 0. G
hence x = 0. G by A1, VECTSP_1:def 18; :: thesis: verum