set TP = TarskiEuclid2Space ;
let a, b, c, x, a1, b1, c1, x1 be POINT of TarskiEuclid2Space; :: according to GTARSKI1:def 9 :: thesis: ( a = b or not a,b,c cong a1,b1,c1 or not between a,b,x or not between a1,b1,x1 or not b,x equiv b1,x1 or c,x equiv c1,x1 )
assume that
A1: a <> b and
A2: a,b,c cong a1,b1,c1 and
A3: between a,b,x and
A4: between a1,b1,x1 and
A5: b,x equiv b1,x1 ; :: thesis: c,x equiv c1,x1
A6: ( dist (a,b) = dist (a1,b1) & dist (a,c) = dist (a1,c1) & dist (b,c) = dist (b1,c1) ) by A2, GTARSKI1:def 15;
A7: dist (a,x) = (dist (a,b)) + (dist (b,x)) by A3, ThConv8;
A8: dist (a1,x1) = (dist (a1,b1)) + (dist (b1,x1)) by A4, ThConv8;
A9: dist (b,x) = dist (b1,x1) by A5, GTARSKI1:def 15;
A10: (dist (c1,x1)) ^2 = (((dist (x1,b1)) ^2) + ((dist (c1,b1)) ^2)) - (((2 * (dist (x1,b1))) * (dist (c1,b1))) * (cos (angle ((Tn2TR x1),(Tn2TR b1),(Tn2TR c1))))) by ThLawOfCosines;
(dist (c,x)) ^2 = (dist (c1,x1)) ^2
proof
per cases ( x = b or c = b or ( x <> b & c <> b ) ) ;
suppose x = b ; :: thesis: (dist (c,x)) ^2 = (dist (c1,x1)) ^2
then A11: 0 = dist (x,b) by ThEgal;
then A12: dist (x1,b1) = 0 by A5, GTARSKI1:def 15;
A12bis: (dist (c,x)) ^2 = ((0 ^2) + ((dist (c,b)) ^2)) - (((2 * 0) * (dist (c,b))) * (cos (angle ((Tn2TR x),(Tn2TR b),(Tn2TR c))))) by A11, ThLawOfCosines
.= (0 * 0) + ((dist (c,b)) ^2) by SQUARE_1:def 1 ;
(dist (c1,x1)) ^2 = ((0 ^2) + ((dist (c1,b1)) ^2)) - (((2 * 0) * (dist (c1,b1))) * (cos (angle ((Tn2TR x1),(Tn2TR b1),(Tn2TR c1))))) by ThLawOfCosines, A12
.= (0 * 0) + ((dist (c1,b1)) ^2) by SQUARE_1:def 1 ;
hence (dist (c,x)) ^2 = (dist (c1,x1)) ^2 by A12bis, A2, GTARSKI1:def 15; :: thesis: verum
end;
suppose A13: c = b ; :: thesis: (dist (c,x)) ^2 = (dist (c1,x1)) ^2
then 0 = dist (c,b) by ThEgal;
then dist (c1,b1) = 0 by A2, GTARSKI1:def 15;
then (dist (c1,x1)) ^2 = (0 * 0) + ((dist (x1,b1)) ^2) by A10, SQUARE_1:def 1;
hence (dist (c,x)) ^2 = (dist (c1,x1)) ^2 by A13, A5, GTARSKI1:def 15; :: thesis: verum
end;
suppose A14: ( x <> b & c <> b ) ; :: thesis: (dist (c,x)) ^2 = (dist (c1,x1)) ^2
A15: a <> x
proof
assume a = x ; :: thesis: contradiction
then (dist (a,b)) + (dist (b,x)) = 0 by A7, ThEgal;
hence contradiction by A1, ThNull; :: thesis: verum
end;
( dist (a,b) <> 0 & dist (a,x) <> 0 & dist (b,x) <> 0 ) by A1, A14, A15, ThEgal;
then A16: ( Tn2TR a1 <> Tn2TR b1 & Tn2TR a1 <> Tn2TR x1 & Tn2TR b1 <> Tn2TR x1 ) by ThEgal, A6, A7, A8, A9;
Tn2TR b in LSeg ((Tn2TR a),(Tn2TR x)) by A3, ThConv6;
then ( (angle ((Tn2TR a),(Tn2TR b),(Tn2TR c))) + (angle ((Tn2TR c),(Tn2TR b),(Tn2TR x))) = PI or (angle ((Tn2TR a),(Tn2TR b),(Tn2TR c))) + (angle ((Tn2TR c),(Tn2TR b),(Tn2TR x))) = 3 * PI ) by A1, A14, EUCLID_6:13;
then ( cos (angle ((Tn2TR a),(Tn2TR b),(Tn2TR c))) = cos (PI - (angle ((Tn2TR c),(Tn2TR b),(Tn2TR x)))) or cos (angle ((Tn2TR a),(Tn2TR b),(Tn2TR c))) = cos ((3 * PI) - (angle ((Tn2TR c),(Tn2TR b),(Tn2TR x)))) ) ;
then A17: cos (angle ((Tn2TR a),(Tn2TR b),(Tn2TR c))) = - (cos (angle ((Tn2TR c),(Tn2TR b),(Tn2TR x)))) by Th2, EUCLID10:2;
Tn2TR b1 in LSeg ((Tn2TR a1),(Tn2TR x1)) by A4, ThConv6;
then ( (angle ((Tn2TR a1),(Tn2TR b1),(Tn2TR c1))) + (angle ((Tn2TR c1),(Tn2TR b1),(Tn2TR x1))) = PI or (angle ((Tn2TR a1),(Tn2TR b1),(Tn2TR c1))) + (angle ((Tn2TR c1),(Tn2TR b1),(Tn2TR x1))) = 3 * PI ) by A16, EUCLID_6:13;
then ( cos (angle ((Tn2TR a1),(Tn2TR b1),(Tn2TR c1))) = cos (PI - (angle ((Tn2TR c1),(Tn2TR b1),(Tn2TR x1)))) or cos (angle ((Tn2TR a1),(Tn2TR b1),(Tn2TR c1))) = cos ((3 * PI) - (angle ((Tn2TR c1),(Tn2TR b1),(Tn2TR x1)))) ) ;
then A18: cos (angle ((Tn2TR a1),(Tn2TR b1),(Tn2TR c1))) = - (cos (angle ((Tn2TR c1),(Tn2TR b1),(Tn2TR x1)))) by Th2, EUCLID10:2;
A19: ( dist (a,b) <> 0 & dist (c,b) <> 0 ) by A1, A14, ThEgal;
A20: (dist (c,a)) ^2 = (((dist (a,b)) ^2) + ((dist (c,b)) ^2)) - (((2 * (dist (a,b))) * (dist (c,b))) * (cos (angle ((Tn2TR a),(Tn2TR b),(Tn2TR c))))) by ThLawOfCosines;
A21: ( dist (a1,b1) <> 0 & dist (c1,b1) <> 0 ) by A1, A6, A14, ThEgal;
(dist (c1,a1)) ^2 = (((dist (a1,b1)) ^2) + ((dist (c1,b1)) ^2)) - (((2 * (dist (a1,b1))) * (dist (c1,b1))) * (cos (angle ((Tn2TR a1),(Tn2TR b1),(Tn2TR c1))))) by ThLawOfCosines;
then A22: cos (angle ((Tn2TR a1),(Tn2TR b1),(Tn2TR c1))) = ((((dist (c,a)) ^2) - ((dist (a,b)) ^2)) - ((dist (c,b)) ^2)) / (- ((2 * (dist (a,b))) * (dist (c,b)))) by A6, Th1, A21
.= cos (angle ((Tn2TR a),(Tn2TR b),(Tn2TR c))) by A20, A19, Th1 ;
(dist (c,x)) ^2 = (((dist (x,b)) ^2) + ((dist (c,b)) ^2)) - (((2 * (dist (x,b))) * (dist (c,b))) * (cos (angle ((Tn2TR x),(Tn2TR b),(Tn2TR c))))) by ThLawOfCosines
.= (((dist (x1,b1)) ^2) + ((dist (c1,b1)) ^2)) - (((2 * (dist (x1,b1))) * (dist (c1,b1))) * (- (cos (angle ((Tn2TR a1),(Tn2TR b1),(Tn2TR c1)))))) by A17, EUCLID_6:3, A6, A9, A22
.= (((dist (x1,b1)) ^2) + ((dist (c1,b1)) ^2)) - (((2 * (dist (x1,b1))) * (dist (c1,b1))) * (cos (angle ((Tn2TR x1),(Tn2TR b1),(Tn2TR c1))))) by A18, EUCLID_6:3
.= (dist (c1,x1)) ^2 by ThLawOfCosines ;
hence (dist (c,x)) ^2 = (dist (c1,x1)) ^2 ; :: thesis: verum
end;
end;
end;
hence c,x equiv c1,x1 by ThConv9; :: thesis: verum