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: 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 ) by ANALOAF:def 2;
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 A2: a,b // c,c ; :: thesis: a = b
reconsider a9 = a, b9 = b, c9 = c as Element of ADG ;
a9,b9 ==> c9,c9 by A1, A2;
hence a = b by Th8; :: 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 A1;
then a9,b9 ==> c9,d9 by Th9;
hence a,b // c,d by A1; :: 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
A3: a9,b9 ==> c9,d9 by Th10;
reconsider d = d9 as Element of (AV ADG) ;
take d ; :: thesis: a,b // c,d
thus a,b // c,d by A1, A3; :: 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 A1;
then q,r ==> q9,r9 by Th11;
hence b,c // b9,c9 by A1; :: 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
A4: a9,b9 ==> b9,c9 by Th12;
reconsider b = b9 as Element of (AV ADG) ;
take b ; :: thesis: a,b // b,c
thus a,b // b,c by A1, A4; :: 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 A1;
hence b = b9 by Th13; :: 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 A1;
then a9,c9 ==> b9,d9 by Th14;
hence a,c // b,d by A1; :: thesis: verum

end;