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 )
set G = Gauge (C,n);
set j = (width (Gauge (C,n))) -' 1;
A1: 2 |^ n >= n + 1 by NEWTON:85;
A2: 1 + (n + 3) > 1 + 0 by XREAL_1:6;
A3: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
A4: len (Gauge (C,n)) = (2 |^ n) + 3 by JORDAN8:def 1;
then A5: len (Gauge (C,n)) >= (n + 1) + 3 by A1, XREAL_1:6;
then len (Gauge (C,n)) > 1 by A2, XXREAL_0:2;
then A6: len (Gauge (C,n)) >= 1 + 1 by NAT_1:13;
then A7: 1 <= (width (Gauge (C,n))) -' 1 by A3, JORDAN5B:2;
A8: ((width (Gauge (C,n))) -' 1) + 1 = len (Gauge (C,n)) by A3, A5, A2, XREAL_1:235, XXREAL_0:2;
then A9: (width (Gauge (C,n))) -' 1 < len (Gauge (C,n)) by NAT_1:13;
assume that
A10: 1 <= i1 and
A11: i1 + 1 <= len (Gauge (C,n)) and
A12: N-min C in cell ((Gauge (C,n)),i1,((width (Gauge (C,n))) -' 1)) and
A13: N-min C <> (Gauge (C,n)) * (i1,((width (Gauge (C,n))) -' 1)) and
A14: 1 <= i2 and
A15: i2 + 1 <= len (Gauge (C,n)) and
A16: N-min C in cell ((Gauge (C,n)),i2,((width (Gauge (C,n))) -' 1)) and
A17: N-min C <> (Gauge (C,n)) * (i2,((width (Gauge (C,n))) -' 1)) and
A18: i1 <> i2 ; :: thesis: contradiction
A19: cell ((Gauge (C,n)),i1,((width (Gauge (C,n))) -' 1)) meets cell ((Gauge (C,n)),i2,((width (Gauge (C,n))) -' 1)) by A12, A16, XBOOLE_0:3;
A20: i1 < len (Gauge (C,n)) by A11, NAT_1:13;
A21: i2 < len (Gauge (C,n)) by A15, NAT_1:13;
per cases ( i1 < i2 or i2 < i1 ) by A18, XXREAL_0:1;
suppose A22: i1 < i2 ; :: thesis: contradiction
then A23: (i2 -' i1) + i1 = i2 by XREAL_1:235;
then i2 -' i1 <= 1 by A21, A3, A19, A7, A9, 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 A20, A3, A6, A9, A22, A23, GOBOARD5:25, JORDAN5B:2;
then A24: 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 A12, A16, XBOOLE_0:def 4;
1 <= ((width (Gauge (C,n))) -' 1) + 1 by NAT_1:12;
then A25: [i2,(((width (Gauge (C,n))) -' 1) + 1)] in Indices (Gauge (C,n)) by A14, A21, A3, A8, MATRIX_0:30;
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 A4, JORDAN8:def 1
.= (2 |^ n) + 2 by NAT_D:34 ;
then A26: (((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge (C,n))) -' 1) - 2) = (N-bound C) - (S-bound C) by A1, XCMPLX_1:87;
[i2,((width (Gauge (C,n))) -' 1)] in Indices (Gauge (C,n)) by A14, A21, A3, A7, A9, MATRIX_0:30;
then A27: (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 A28: ((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 A25, 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 A28, SPPOL_1:16;
then (N-min C) `1 = ((Gauge (C,n)) * (i2,((width (Gauge (C,n))) -' 1))) `1 by A24, SPPOL_1:41;
hence contradiction by A17, A27, A28, A26, EUCLID:52; :: thesis: verum
end;
suppose A29: i2 < i1 ; :: thesis: contradiction
then A30: (i1 -' i2) + i2 = i1 by XREAL_1:235;
then i1 -' i2 <= 1 by A20, A3, A19, A7, A9, 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 A21, A3, A6, A9, A29, A30, GOBOARD5:25, JORDAN5B:2;
then A31: 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 A12, A16, XBOOLE_0:def 4;
1 <= ((width (Gauge (C,n))) -' 1) + 1 by NAT_1:12;
then A32: [i1,(((width (Gauge (C,n))) -' 1) + 1)] in Indices (Gauge (C,n)) by A10, A20, A3, A8, MATRIX_0:30;
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 A4, JORDAN8:def 1
.= (2 |^ n) + 2 by NAT_D:34 ;
then A33: (((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge (C,n))) -' 1) - 2) = (N-bound C) - (S-bound C) by A1, XCMPLX_1:87;
[i1,((width (Gauge (C,n))) -' 1)] in Indices (Gauge (C,n)) by A10, A20, A3, A7, A9, MATRIX_0:30;
then A34: (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 A35: ((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 A32, 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 A35, SPPOL_1:16;
then (N-min C) `1 = ((Gauge (C,n)) * (i1,((width (Gauge (C,n))) -' 1))) `1 by A31, SPPOL_1:41;
hence contradiction by A13, A34, A35, A33, EUCLID:52; :: thesis: verum
end;
end;