let ADG be Uniquely_Two_Divisible_Group; :: thesis:
assume A1: ex a, b being Element of ADG st a <> b ; :: thesis:
set A = AV ADG;
A2: AV ADG = AffinStruct(# the carrier of ADG,(CONGRD ADG) #) ;
A3: for a', b', c', d' being Element of (AV ADG)
for a, b, c, d being Element of ADG st a = a' & b = b' & c = c' & d = d' holds
( a,b ==> c,d iff a',b' // c',d' )

let a', b', c', d' be Element of (AV ADG); :: thesis:
let a, b, c, d be Element of ADG; :: thesis:
assume A4: ( a = a' & b = b' & c = c' & d = d' ) ; :: thesis:

A5: now

assume a,b ==> c,d ; :: thesis:
then [[a,b],[c,d]] in CONGRD ADG by A2, Def6;
hence a',b' // c',d' by A4, ANALOAF:def 2; :: thesis:

end;

now

assume a',b' // c',d' ; :: thesis:
then [[a,b],[c,d]] in CONGRD ADG by A4, ANALOAF:def 2;
hence a,b ==> c,d by A2, Def6; :: thesis:

end;

hence ( a,b ==> c,d iff a',b' // c',d' ) by A5; :: thesis:

end;

thus ex a, b being Element of (AV ADG) st a <> b by A1; :: thesis:
thus for a, b, c being Element of (AV ADG) st a,b // c,c holds
a = b :: thesis:

let a, b, c be Element of (AV ADG); :: thesis:
assume A6: a,b // c,c ; :: thesis:
reconsider a' = a, b' = b, c' = c as Element of ADG ;
a',b' ==> c',c' by A3, A6;
hence a = b by Th13; :: thesis:

end;

thus for a, b, c, d, p, q being Element of (AV ADG) st a,b // p,q & c,d // p,q holds
a,b // c,d :: thesis:

let a, b, c, d, p, q be Element of (AV ADG); :: thesis:
assume A7: ( a,b // p,q & c,d // p,q ) ; :: thesis:
reconsider a' = a, b' = b, c' = c, d' = d, p' = p, q' = q as Element of ADG ;
( a',b' ==> p',q' & c',d' ==> p',q' ) by A3, A7;
then a',b' ==> c',d' by Th14;
hence a,b // c,d by A3; :: thesis:

end;

thus for a, b, c being Element of (AV ADG) ex d being Element of (AV ADG) st a,b // c,d :: thesis:

let a, b, c be Element of (AV ADG); :: thesis:
reconsider a' = a, b' = b, c' = c as Element of ADG ;
consider d' being Element of ADG such that
A8: a',b' ==> c',d' by Th15;
reconsider d = d' as Element of (AV ADG) ;
take d ; :: thesis:
thus a,b // c,d by A3, A8; :: thesis:

end;

thus for a, b, c, a', b', c' being Element of (AV ADG) st a,b // a',b' & a,c // a',c' holds
b,c // b',c' :: thesis:

let a, b, c, a', b', c' be Element of (AV ADG); :: thesis:
assume A9: ( a,b // a',b' & a,c // a',c' ) ; :: thesis:
reconsider p = a, q = b, r = c, p' = a', q' = b', r' = c' as Element of ADG ;
( p,q ==> p',q' & p,r ==> p',r' ) by A3, A9;
then q,r ==> q',r' by Th16;
hence b,c // b',c' by A3; :: thesis:

end;

thus for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c :: thesis:

let a, c be Element of (AV ADG); :: thesis:
reconsider a' = a, c' = c as Element of ADG ;
consider b' being Element of the carrier of ADG such that
A10: a',b' ==> b',c' by Th17;
reconsider b = b' as Element of (AV ADG) ;
take b ; :: thesis:
thus a,b // b,c by A3, A10; :: thesis:

end;

thus for a, b, c, b' being Element of (AV ADG) st a,b // b,c & a,b' // b',c holds
b = b' :: thesis:

let a, b, c, b' be Element of (AV ADG); :: thesis:
assume A11: ( a,b // b,c & a,b' // b',c ) ; :: thesis:
reconsider a' = a, p = b, c' = c, p' = b' as Element of ADG ;
( a',p ==> p,c' & a',p' ==> p',c' ) by A3, A11;
hence b = b' by Th18; :: thesis:

end;

thus for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d :: thesis:

let a, b, c, d be Element of (AV ADG); :: thesis:
assume A12: a,b // c,d ; :: thesis:
reconsider a' = a, b' = b, c' = c, d' = d as Element of ADG ;
a',b' ==> c',d' by A3, A12;
then a',c' ==> b',d' by Th19;
hence a,c // b,d by A3; :: thesis:

end;