let ADG be Uniquely_Two_Divisible_Group; :: thesis: ( ex a, b being Element of ADG st a <> b implies ( ex a, b being Element of (AV ADG) st a <> b & ( for a, b, c being Element of (AV ADG) st a,b // c,c holds
a = b ) & ( 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 ) & ( for a, b, c being Element of (AV ADG) ex d being Element of (AV ADG) st a,b // c,d ) & ( for a, b, c, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) ) )
set A = AV ADG;
assume ex a, b being Element of ADG st a <> b ; :: thesis: ( ex a, b being Element of (AV ADG) st a <> b & ( for a, b, c being Element of (AV ADG) st a,b // c,c holds
a = b ) & ( 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 ) & ( for a, b, c being Element of (AV ADG) ex d being Element of (AV ADG) st a,b // c,d ) & ( for a, b, c, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) )
hence ex a, b being Element of (AV ADG) st a <> b ; :: thesis: ( ( for a, b, c being Element of (AV ADG) st a,b // c,c holds
a = b ) & ( 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 ) & ( for a, b, c being Element of (AV ADG) ex d being Element of (AV ADG) st a,b // c,d ) & ( for a, b, c, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) )
A1: AV ADG = AffinStruct(# the carrier of ADG,(CONGRD ADG) #) ;
A2: for a9, b9, c9, d9 being Element of (AV ADG)
for a, b, c, d being Element of ADG st a = a9 & b = b9 & c = c9 & d = d9 holds
( a,b ==> c,d iff a9,b9 // c9,d9 )

proof

let a9, b9, c9, d9 be Element of (AV ADG); :: thesis: for a, b, c, d being Element of ADG st a = a9 & b = b9 & c = c9 & d = d9 holds
( a,b ==> c,d iff a9,b9 // c9,d9 )
let a, b, c, d be Element of ADG; :: thesis: ( a = a9 & b = b9 & c = c9 & d = d9 implies ( a,b ==> c,d iff a9,b9 // c9,d9 ) )
assume A3: ( a = a9 & b = b9 & c = c9 & d = d9 ) ; :: thesis: ( a,b ==> c,d iff a9,b9 // c9,d9 )

A4: now

assume a9,b9 // c9,d9 ; :: thesis: a,b ==> c,d
then [[a,b],[c,d]] in CONGRD ADG by A3, ANALOAF:def 2;
hence a,b ==> c,d by A1, Def6; :: thesis: verum

end;

now

assume a,b ==> c,d ; :: thesis: a9,b9 // c9,d9
then [[a,b],[c,d]] in CONGRD ADG by A1, Def6;
hence a9,b9 // c9,d9 by A3, ANALOAF:def 2; :: thesis: verum

end;

hence ( a,b ==> c,d iff a9,b9 // c9,d9 ) by A4; :: thesis: verum

end;

thus for a, b, c being Element of (AV ADG) st a,b // c,c holds
a = b :: thesis: ( ( 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 ) & ( for a, b, c being Element of (AV ADG) ex d being Element of (AV ADG) st a,b // c,d ) & ( for a, b, c, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) )

proof

let a, b, c be Element of (AV ADG); :: thesis: ( a,b // c,c implies a = b )
assume A5: a,b // c,c ; :: thesis: a = b
reconsider a9 = a, b9 = b, c9 = c as Element of ADG ;
a9,b9 ==> c9,c9 by A2, A5;
hence a = b by Th13; :: thesis: verum

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: ( ( for a, b, c being Element of (AV ADG) ex d being Element of (AV ADG) st a,b // c,d ) & ( for a, b, c, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) )

proof

let a, b, c, d, p, q be Element of (AV ADG); :: thesis: ( a,b // p,q & c,d // p,q implies a,b // c,d )
reconsider a9 = a, b9 = b, c9 = c, d9 = d, p9 = p, q9 = q as Element of ADG ;
assume ( a,b // p,q & c,d // p,q ) ; :: thesis: a,b // c,d
then ( a9,b9 ==> p9,q9 & c9,d9 ==> p9,q9 ) by A2;
then a9,b9 ==> c9,d9 by Th14;
hence a,b // c,d by A2; :: thesis: verum

end;

thus for a, b, c being Element of (AV ADG) ex d being Element of (AV ADG) st a,b // c,d :: thesis: ( ( for a, b, c, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) )

proof

let a, b, c be Element of (AV ADG); :: thesis: ex d being Element of (AV ADG) st a,b // c,d
reconsider a9 = a, b9 = b, c9 = c as Element of ADG ;
consider d9 being Element of ADG such that
A6: a9,b9 ==> c9,d9 by Th15;
reconsider d = d9 as Element of (AV ADG) ;
take d ; :: thesis: a,b // c,d
thus a,b // c,d by A2, A6; :: thesis: verum

end;

thus for a, b, c, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 :: thesis: ( ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) )

proof

let a, b, c, a9, b9, c9 be Element of (AV ADG); :: thesis: ( a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
reconsider p = a, q = b, r = c, p9 = a9, q9 = b9, r9 = c9 as Element of ADG ;
assume ( a,b // a9,b9 & a,c // a9,c9 ) ; :: thesis: b,c // b9,c9
then ( p,q ==> p9,q9 & p,r ==> p9,r9 ) by A2;
then q,r ==> q9,r9 by Th16;
hence b,c // b9,c9 by A2; :: thesis: verum

end;

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

proof

let a, c be Element of (AV ADG); :: thesis: ex b being Element of (AV ADG) st a,b // b,c
reconsider a9 = a, c9 = c as Element of ADG ;
consider b9 being Element of ADG such that
A7: a9,b9 ==> b9,c9 by Th17;
reconsider b = b9 as Element of (AV ADG) ;
take b ; :: thesis: a,b // b,c
thus a,b // b,c by A2, A7; :: thesis: verum

end;

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

proof

let a, b, c, b9 be Element of (AV ADG); :: thesis: ( a,b // b,c & a,b9 // b9,c implies b = b9 )
reconsider a9 = a, p = b, c9 = c, p9 = b9 as Element of ADG ;
assume ( a,b // b,c & a,b9 // b9,c ) ; :: thesis: b = b9
then ( a9,p ==> p,c9 & a9,p9 ==> p9,c9 ) by A2;
hence b = b9 by Th18; :: thesis: verum

end;

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

proof

let a, b, c, d be Element of (AV ADG); :: thesis: ( a,b // c,d implies a,c // b,d )
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of ADG ;
assume a,b // c,d ; :: thesis: a,c // b,d
then a9,b9 ==> c9,d9 by A2;
then a9,c9 ==> b9,d9 by Th19;
hence a,c // b,d by A2; :: thesis: verum

end;