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

proof

let a', b', c', d' be Element of ; :: thesis: for a, b, c, d being Element of 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 ; :: thesis: ( a = a' & b = b' & c = c' & d = d' implies ( a,b ==> c,d iff a',b' // c',d' ) )
assume A3: ( a = a' & b = b' & c = c' & d = d' ) ; :: thesis: ( a,b ==> c,d iff a',b' // c',d' )

A4: now

assume a',b' // c',d' ; :: 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: a',b' // c',d'
then [[a,b],[c,d]] in CONGRD ADG by A1, Def6;
hence a',b' // c',d' by A3, ANALOAF:def 2; :: thesis: verum

end;

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

let a, b, c be Element of ; :: thesis: ex d being Element of st a,b // c,d
reconsider a' = a, b' = b, c' = c as Element of ;
consider d' being Element of such that
A6: a',b' ==> c',d' by Th15;
reconsider d = d' as Element of ;
take d ; :: thesis: a,b // c,d
thus a,b // c,d by A2, A6; :: thesis: verum

end;

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

proof

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

end;

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

proof

let a, c be Element of ; :: thesis: ex b being Element of st a,b // b,c
reconsider a' = a, c' = c as Element of ;
consider b' being Element of such that
A7: a',b' ==> b',c' by Th17;
reconsider b = b' as Element of ;
take b ; :: thesis: a,b // b,c
thus a,b // b,c by A2, A7; :: thesis: verum

end;

thus for a, b, c, b' being Element of st a,b // b,c & a,b' // b',c holds
b = b' :: thesis: for a, b, c, d being Element of st a,b // c,d holds
a,c // b,d

proof

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

end;

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

proof

let a, b, c, d be Element of ; :: thesis: ( a,b // c,d implies a,c // b,d )
reconsider a' = a, b' = b, c' = c, d' = d as Element of ;
assume a,b // c,d ; :: thesis: a,c // b,d
then a',b' ==> c',d' by A2;
then a',c' ==> b',d' by Th19;
hence a,c // b,d by A2; :: thesis: verum

end;