let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n, i1, i2 being Nat st 1 <= i1 & i1 + 1 <= len (Gauge C,n) & N-min C in cell (Gauge C,n),i1,((width (Gauge C,n)) -' 1) & N-min C <> (Gauge C,n) * i1,((width (Gauge C,n)) -' 1) & 1 <= i2 & i2 + 1 <= len (Gauge C,n) & N-min C in cell (Gauge C,n),i2,((width (Gauge C,n)) -' 1) & N-min C <> (Gauge C,n) * i2,((width (Gauge C,n)) -' 1) holds
i1 = i2
let n, i1, i2 be Nat; :: thesis: ( 1 <= i1 & i1 + 1 <= len (Gauge C,n) & N-min C in cell (Gauge C,n),i1,((width (Gauge C,n)) -' 1) & N-min C <> (Gauge C,n) * i1,((width (Gauge C,n)) -' 1) & 1 <= i2 & i2 + 1 <= len (Gauge C,n) & N-min C in cell (Gauge C,n),i2,((width (Gauge C,n)) -' 1) & N-min C <> (Gauge C,n) * i2,((width (Gauge C,n)) -' 1) implies i1 = i2 )
A1: i1 in NAT by ORDINAL1:def 13;
set G = Gauge C,n;
set j = (width (Gauge C,n)) -' 1;
A2: i2 in NAT by ORDINAL1:def 13;
A3: 2 |^ n >= n + 1 by NEWTON:104;
A4: 1 + (n + 3) > 1 + 0 by XREAL_1:8;
A5: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
A6: len (Gauge C,n) = (2 |^ n) + 3 by JORDAN8:def 1;
then A7: len (Gauge C,n) >= (n + 1) + 3 by A3, XREAL_1:8;
then len (Gauge C,n) > 1 by A4, XXREAL_0:2;
then A8: len (Gauge C,n) >= 1 + 1 by NAT_1:13;
then A9: 1 <= (width (Gauge C,n)) -' 1 by A5, JORDAN5B:2;
A10: ((width (Gauge C,n)) -' 1) + 1 = len (Gauge C,n) by A5, A7, A4, XREAL_1:237, XXREAL_0:2;
then A11: (width (Gauge C,n)) -' 1 < len (Gauge C,n) by NAT_1:13;
assume that
A12: 1 <= i1 and
A13: i1 + 1 <= len (Gauge C,n) and
A14: N-min C in cell (Gauge C,n),i1,((width (Gauge C,n)) -' 1) and
A15: N-min C <> (Gauge C,n) * i1,((width (Gauge C,n)) -' 1) and
A16: 1 <= i2 and
A17: i2 + 1 <= len (Gauge C,n) and
A18: N-min C in cell (Gauge C,n),i2,((width (Gauge C,n)) -' 1) and
A19: N-min C <> (Gauge C,n) * i2,((width (Gauge C,n)) -' 1) and
A20: i1 <> i2 ; :: thesis: contradiction
A21: cell (Gauge C,n),i1,((width (Gauge C,n)) -' 1) meets cell (Gauge C,n),i2,((width (Gauge C,n)) -' 1) by A14, A18, XBOOLE_0:3;
A22: i1 < len (Gauge C,n) by A13, NAT_1:13;
A23: i2 < len (Gauge C,n) by A17, NAT_1:13;

per cases ( i1 < i2 or i2 < i1 ) by A20, XXREAL_0:1;

suppose A24: i1 < i2 ; :: thesis: contradiction

then A25: (i2 -' i1) + i1 = i2 by XREAL_1:237;
then i2 -' i1 <= 1 by A1, A23, A5, A21, A9, A11, JORDAN8:10;
then ( i2 -' i1 < 1 or i2 -' i1 = 1 ) by XXREAL_0:1;
then ( i2 -' i1 = 0 or i2 -' i1 = 1 ) by NAT_1:14;
then (cell (Gauge C,n),i1,((width (Gauge C,n)) -' 1)) /\ (cell (Gauge C,n),i2,((width (Gauge C,n)) -' 1)) = LSeg ((Gauge C,n) * i2,((width (Gauge C,n)) -' 1)),((Gauge C,n) * i2,(((width (Gauge C,n)) -' 1) + 1)) by A1, A22, A5, A8, A11, A24, A25, GOBOARD5:26, JORDAN5B:2;
then A26: N-min C in LSeg ((Gauge C,n) * i2,((width (Gauge C,n)) -' 1)),((Gauge C,n) * i2,(((width (Gauge C,n)) -' 1) + 1)) by A14, A18, XBOOLE_0:def 4;
1 <= ((width (Gauge C,n)) -' 1) + 1 by NAT_1:12;
then A27: [i2,(((width (Gauge C,n)) -' 1) + 1)] in Indices (Gauge C,n) by A16, A23, A5, A10, MATRIX_1:37;
set y2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 1));
set y1 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 2));
set x = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2));
(width (Gauge C,n)) -' 1 = (((2 |^ n) + 2) + 1) -' 1 by A6, JORDAN8:def 1
.= (2 |^ n) + 2 by NAT_D:34 ;
then A28: (((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 2) = (N-bound C) - (S-bound C) by A3, XCMPLX_1:88;
[i2,((width (Gauge C,n)) -' 1)] in Indices (Gauge C,n) by A16, A23, A5, A9, A11, MATRIX_1:37;
then A29: (Gauge C,n) * i2,((width (Gauge C,n)) -' 1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 2)))]| by JORDAN8:def 1;
then A30: ((Gauge C,n) * i2,((width (Gauge C,n)) -' 1)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2)) by EUCLID:56;
(((width (Gauge C,n)) -' 1) + 1) - (1 + 1) = ((width (Gauge C,n)) -' 1) - 1 ;
then (Gauge C,n) * i2,(((width (Gauge C,n)) -' 1) + 1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 1)))]| by A27, JORDAN8:def 1;
then ((Gauge C,n) * i2,(((width (Gauge C,n)) -' 1) + 1)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2)) by EUCLID:56;
then LSeg ((Gauge C,n) * i2,((width (Gauge C,n)) -' 1)),((Gauge C,n) * i2,(((width (Gauge C,n)) -' 1) + 1)) is vertical by A30, SPPOL_1:37;
then (N-min C) `1 = ((Gauge C,n) * i2,((width (Gauge C,n)) -' 1)) `1 by A26, SPPOL_1:64;
hence contradiction by A19, A29, A30, A28, EUCLID:56; :: thesis: verum

end;

suppose A31: i2 < i1 ; :: thesis: contradiction

then A32: (i1 -' i2) + i2 = i1 by XREAL_1:237;
then i1 -' i2 <= 1 by A2, A22, A5, A21, A9, A11, JORDAN8:10;
then ( i1 -' i2 < 1 or i1 -' i2 = 1 ) by XXREAL_0:1;
then ( i1 -' i2 = 0 or i1 -' i2 = 1 ) by NAT_1:14;
then (cell (Gauge C,n),i2,((width (Gauge C,n)) -' 1)) /\ (cell (Gauge C,n),i1,((width (Gauge C,n)) -' 1)) = LSeg ((Gauge C,n) * i1,((width (Gauge C,n)) -' 1)),((Gauge C,n) * i1,(((width (Gauge C,n)) -' 1) + 1)) by A2, A23, A5, A8, A11, A31, A32, GOBOARD5:26, JORDAN5B:2;
then A33: N-min C in LSeg ((Gauge C,n) * i1,((width (Gauge C,n)) -' 1)),((Gauge C,n) * i1,(((width (Gauge C,n)) -' 1) + 1)) by A14, A18, XBOOLE_0:def 4;
1 <= ((width (Gauge C,n)) -' 1) + 1 by NAT_1:12;
then A34: [i1,(((width (Gauge C,n)) -' 1) + 1)] in Indices (Gauge C,n) by A12, A22, A5, A10, MATRIX_1:37;
set y2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 1));
set y1 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 2));
set x = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2));
(width (Gauge C,n)) -' 1 = (((2 |^ n) + 2) + 1) -' 1 by A6, JORDAN8:def 1
.= (2 |^ n) + 2 by NAT_D:34 ;
then A35: (((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 2) = (N-bound C) - (S-bound C) by A3, XCMPLX_1:88;
[i1,((width (Gauge C,n)) -' 1)] in Indices (Gauge C,n) by A12, A22, A5, A9, A11, MATRIX_1:37;
then A36: (Gauge C,n) * i1,((width (Gauge C,n)) -' 1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 2)))]| by JORDAN8:def 1;
then A37: ((Gauge C,n) * i1,((width (Gauge C,n)) -' 1)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2)) by EUCLID:56;
(((width (Gauge C,n)) -' 1) + 1) - (1 + 1) = ((width (Gauge C,n)) -' 1) - 1 ;
then (Gauge C,n) * i1,(((width (Gauge C,n)) -' 1) + 1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 1)))]| by A34, JORDAN8:def 1;
then ((Gauge C,n) * i1,(((width (Gauge C,n)) -' 1) + 1)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2)) by EUCLID:56;
then LSeg ((Gauge C,n) * i1,((width (Gauge C,n)) -' 1)),((Gauge C,n) * i1,(((width (Gauge C,n)) -' 1) + 1)) is vertical by A37, SPPOL_1:37;
then (N-min C) `1 = ((Gauge C,n) * i1,((width (Gauge C,n)) -' 1)) `1 by A33, SPPOL_1:64;
hence contradiction by A15, A36, A37, A35, EUCLID:56; :: thesis: verum

end;

end;