let ADG be Uniquely_Two_Divisible_Group; :: thesis: 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; :: thesis: ex d being Element of ADG st a,b ==> c,d
set d9 = (- a) + (b + c);
take (- a) + (b + c) ; :: thesis: 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; :: thesis: verum