let ADG be Uniquely_Two_Divisible_Group; for a, b, c being Element of ADG ex d being Element of ADG st a,b ==> c,d
let a, b, c be Element of ADG; ex d being Element of ADG st a,b ==> c,d
set d9 = (- a) + (b + c);
take
(- a) + (b + c)
; a,b ==> c,(- a) + (b + c)
a + ((- a) + (b + c)) =
(a + (- a)) + (b + c)
by RLVECT_1:def 3
.=
(0. ADG) + (b + c)
by RLVECT_1:5
.=
b + c
by RLVECT_1:4
;
hence
a,b ==> c,(- a) + (b + c)
by Th5; verum