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