let ADG be Uniquely_Two_Divisible_Group; :: thesis: for a, c being Element of ADG ex b being Element of ADG st a,b ==> b,c
let a, c be Element of ADG; :: thesis: ex b being Element of ADG st a,b ==> b,c
consider b being Element of ADG such that
A1: b + b = a + c by Def1;
take b ; :: thesis: a,b ==> b,c
thus a,b ==> b,c by A1, Th5; :: thesis: verum