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