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 12;
set G = Gauge (C,n);
set j = (width (Gauge (C,n))) -' 1;
A2: i2 in NAT by ORDINAL1:def 12;
A3: 2 |^ n >= n + 1 by NEWTON:85;
A4: 1 + (n + 3) > 1 + 0 by XREAL_1:6;
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:6;
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:235, 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:235;
then i2 -' i1 <= 1 by A1, A23, A5, A21, A9, A11, JORDAN8:7;
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:25, 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:36;
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:87;
[i2,((width (Gauge (C,n))) -' 1)] in Indices (Gauge (C,n)) by A16, A23, A5, A9, A11, MATRIX_1:36;
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:52;
(((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:52;
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:16;
then (N-min C) `1 = ((Gauge (C,n)) * (i2,((width (Gauge (C,n))) -' 1))) `1 by A26, SPPOL_1:41;
hence contradiction by A19, A29, A30, A28, EUCLID:52; :: thesis: verum

end;

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

then A32: (i1 -' i2) + i2 = i1 by XREAL_1:235;
then i1 -' i2 <= 1 by A2, A22, A5, A21, A9, A11, JORDAN8:7;
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:25, 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:36;
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:87;
[i1,((width (Gauge (C,n))) -' 1)] in Indices (Gauge (C,n)) by A12, A22, A5, A9, A11, MATRIX_1:36;
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:52;
(((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:52;
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:16;
then (N-min C) `1 = ((Gauge (C,n)) * (i1,((width (Gauge (C,n))) -' 1))) `1 by A33, SPPOL_1:41;
hence contradiction by A15, A36, A37, A35, EUCLID:52; :: thesis: verum

end;

end;