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

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