let ADG be Uniquely_Two_Divisible_Group; :: thesis: for a, b, c, a9, b9, c9 being Element of ADG st a,b ==> a9,b9 & a,c ==> a9,c9 holds
b,c ==> b9,c9
let a, b, c, a9, b9, c9 be Element of ADG; :: thesis: ( a,b ==> a9,b9 & a,c ==> a9,c9 implies b,c ==> b9,c9 )
assume ( a,b ==> a9,b9 & a,c ==> a9,c9 ) ; :: thesis: b,c ==> b9,c9
then ( a + b9 = b + a9 & a + c9 = c + a9 ) by Th5;
then b + (a9 + (a + c9)) = (c + a9) + (a + b9) by RLVECT_1:def 3
.= c + (a9 + (a + b9)) by RLVECT_1:def 3 ;
then b + ((a9 + a) + c9) = c + (a9 + (a + b9)) by RLVECT_1:def 3
.= c + ((a9 + a) + b9) by RLVECT_1:def 3 ;
then (b + c9) + (a9 + a) = c + (b9 + (a9 + a)) by RLVECT_1:def 3
.= (c + b9) + (a9 + a) by RLVECT_1:def 3 ;
then b + c9 = c + b9 by RLVECT_1:8;
hence b,c ==> b9,c9 by Th5; :: thesis: verum