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 d' = (- a) + (b + c);
A1: a + ((- a) + (b + c)) = (a + (- a)) + (b + c) by RLVECT_1:def 6
.= (0. ADG) + (b + c) by RLVECT_1:16
.= b + c by RLVECT_1:10 ;
take d = (- a) + (b + c); :: thesis: a,b ==> c,d
thus a,b ==> c,d by A1, Th10; :: thesis: verum