let ADG be Uniquely_Two_Divisible_Group; 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; ( 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
; 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; verum