let ADG be Uniquely_Two_Divisible_Group; :: thesis: for a, b, c being Element of ADG st a,b ==> c,c holds
a = b
let a, b, c be Element of ADG; :: thesis: ( a,b ==> c,c implies a = b )
assume a,b ==> c,c ; :: thesis: a = b
then a # c = b # c by Th5;
hence a = b by RLVECT_1:8; :: thesis: verum