let ADG be Uniquely_Two_Divisible_Group; :: thesis: for a, b, c, d, p, q being Element of ADG st a,b ==> p,q & c,d ==> p,q holds
a,b ==> c,d
let a, b, c, d, p, q be Element of ADG; :: thesis: ( a,b ==> p,q & c,d ==> p,q implies a,b ==> c,d )
assume that
A1: a,b ==> p,q and
A2: c,d ==> p,q ; :: thesis: a,b ==> c,d
a # q = b # p by A1, Th5;
then a + (q + d) = (b + p) + d by RLVECT_1:def 3
.= b + (p + d) by RLVECT_1:def 3
.= b + (c + q) by A2, Th5 ;
then (a + d) + q = b + (c + q) by RLVECT_1:def 3
.= (b + c) + q by RLVECT_1:def 3 ;
then a + d = b + c by RLVECT_1:8;
hence a,b ==> c,d by Th5; :: thesis: verum