let L be non empty addLoopStr ; :: thesis: for a, b being Element of L st ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & a + b = 0. L holds
b + a = 0. L
let a, b be Element of L; :: thesis: ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & a + b = 0. L implies b + a = 0. L )
assume A1: ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) ) ; :: thesis: ( not a + b = 0. L or b + a = 0. L )
assume A2: a + b = 0. L ; :: thesis: b + a = 0. L
consider x being Element of L such that
A3: b + x = 0. L by A1;
thus b + a = (b + a) + (b + x) by A1, A3
.= ((b + a) + b) + x by A1
.= (b + (0. L)) + x by A1, A2
.= 0. L by A1, A3 ; :: thesis: verum