let ADG be Uniquely_Two_Divisible_Group; :: thesis: for a, b, c, b' being Element of ADG st a,b ==> b,c & a,b' ==> b',c holds
b = b'
let a, b, c, b' be Element of ADG; :: thesis: ( a,b ==> b,c & a,b' ==> b',c implies b = b' )
assume ( a,b ==> b,c & a,b' ==> b',c ) ; :: thesis: b = b'
then ( a + c = b + b & a + c = b' + b' ) by Th10;
then (b + (- b')) + b = (b' + b') + (- b') by RLVECT_1:def 6
.= b' + (b' + (- b')) by RLVECT_1:def 6
.= b' + (0. ADG) by RLVECT_1:16
.= b' by RLVECT_1:10 ;
then A1: (b + (- b')) + (b + (- b')) = b' + (- b') by RLVECT_1:def 6
.= 0. ADG by RLVECT_1:16 ;
b' = (0. ADG) + b' by RLVECT_1:10
.= (b + (- b')) + b' by A1, VECTSP_1:def 28
.= b + ((- b') + b') by RLVECT_1:def 6
.= b + (0. ADG) by RLVECT_1:16
.= b by RLVECT_1:10 ;
hence b = b' ; :: thesis: verum