let i, n be Nat; :: thesis:
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
let p, x be Point of (TOP-REAL 2); :: thesis:
set G = Gauge (C,n);
set f = Cage (C,n);
assume that
A1: x in W-most C and
A2: p in west_halfline x and
A3: 1 <= i and
A4: i < len (Cage (C,n)) and
A5: p in LSeg ((Cage (C,n)),i) ; :: thesis:
assume A6: not LSeg ((Cage (C,n)),i) is vertical ; :: thesis:
A7: i + 1 <= len (Cage (C,n)) by A4, NAT_1:13;
then A8: LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A3, TOPREAL1:def 3;
1 <= i + 1 by A3, NAT_1:13;
then i + 1 in Seg (len (Cage (C,n))) by A7, FINSEQ_1:1;
then A9: i + 1 in dom (Cage (C,n)) by FINSEQ_1:def 3;
p in L~ (Cage (C,n)) by A5, SPPOL_2:17;
then A10: p in (west_halfline x) /\ (L~ (Cage (C,n))) by A2, XBOOLE_0:def 4;
A11: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
A12: x `2 = p `2 by A2, TOPREAL1:def 13
.= ((Cage (C,n)) /. i) `2 by A5, A8, A6, SPPOL_1:19, SPPOL_1:40 ;
i in Seg (len (Cage (C,n))) by A3, A4, FINSEQ_1:1;
then A13: i in dom (Cage (C,n)) by FINSEQ_1:def 3;
A14: x `2 = p `2 by A2, TOPREAL1:def 13
.= ((Cage (C,n)) /. (i + 1)) `2 by A5, A8, A6, SPPOL_1:19, SPPOL_1:40 ;
A15: x in C by A1, XBOOLE_0:def 4;

per cases ) /. i) `1 <= ((Cage (C,n)) /. (i + 1)) `1 or ((Cage (C,n)) /. i) `1 >= ((Cage (C,n)) /. (i + 1)) `1 ) ;

suppose A16: ((Cage (C,n)) /. i) `1 <= ((Cage (C,n)) /. (i + 1)) `1 ; :: thesis:

consider i1, i2 being Nat such that
A17: [i1,i2] in Indices (Gauge (C,n)) and
A18: (Cage (C,n)) /. i = (Gauge (C,n)) * (i1,i2) by A11, A13, GOBOARD1:def 9;
A19: 1 <= i2 by A17, MATRIX_0:32;
A20: i2 <= width (Gauge (C,n)) by A17, MATRIX_0:32;
then A21: i2 <= len (Gauge (C,n)) by JORDAN8:def 1;
consider j1, j2 being Nat such that
A22: [j1,j2] in Indices (Gauge (C,n)) and
A23: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (j1,j2) by A11, A9, GOBOARD1:def 9;
A24: ( 1 <= j2 & j2 <= width (Gauge (C,n)) ) by A22, MATRIX_0:32;

now :: thesis:

assume ((Cage (C,n)) /. i) `1 = ((Cage (C,n)) /. (i + 1)) `1 ; :: thesis:
then A25: (Cage (C,n)) /. i = (Cage (C,n)) /. (i + 1) by A14, A12, TOPREAL3:6;
then A26: i1 = j1 by A17, A18, A22, A23, GOBOARD1:5;
A27: i2 = j2 by A17, A18, A22, A23, A25, GOBOARD1:5;
|.(i1 - j1).| + |.(i2 - j2).| = 1 by A11, A13, A9, A17, A18, A22, A23, GOBOARD1:def 9;
then 1 = 0 + |.(i2 - j2).| by A26, GOBOARD7:2
.= 0 + 0 by A27, GOBOARD7:2 ;
hence contradiction ; :: thesis:

end;

then A28: ((Cage (C,n)) /. i) `1 < ((Cage (C,n)) /. (i + 1)) `1 by A16, XXREAL_0:1;
((Cage (C,n)) /. i) `1 <= p `1 by A5, A8, A16, TOPREAL1:3;
then A29: ((Cage (C,n)) /. i) `1 < x `1 by A15, A10, Th77, XXREAL_0:2;
A30: 1 <= i1 by A17, MATRIX_0:32;
A31: i1 <= len (Gauge (C,n)) by A17, MATRIX_0:32;
A32: x `1 = (W-min C) `1 by A1, PSCOMP_1:31
.= W-bound C by EUCLID:52
.= ((Gauge (C,n)) * (2,i2)) `1 by A19, A21, JORDAN8:11 ;
then i1 < 1 + 1 by A29, A18, A19, A20, A31, SPRECT_3:13;
then A33: i1 <= 1 by NAT_1:13;
A34: j1 <= len (Gauge (C,n)) by A22, MATRIX_0:32;
1 <= j1 by A22, MATRIX_0:32;
then i1 < j1 by A18, A19, A20, A31, A23, A24, A28, Th18;
then 1 < j1 by A30, A33, XXREAL_0:1;
then 1 + 1 <= j1 by NAT_1:13;
then x `1 <= ((Cage (C,n)) /. (i + 1)) `1 by A19, A20, A32, A23, A24, A34, Th18;
then x in L~ (Cage (C,n)) by A8, A14, A12, A29, GOBOARD7:8, SPPOL_2:17;
then x in (L~ (Cage (C,n))) /\ C by A15, XBOOLE_0:def 4;
then L~ (Cage (C,n)) meets C ;
hence contradiction by JORDAN10:5; :: thesis:

end;

suppose A35: ((Cage (C,n)) /. i) `1 >= ((Cage (C,n)) /. (i + 1)) `1 ; :: thesis:

consider i1, i2 being Nat such that
A36: [i1,i2] in Indices (Gauge (C,n)) and
A37: (Cage (C,n)) /. (i + 1) = (Gauge (C,n)) * (i1,i2) by A11, A9, GOBOARD1:def 9;
A38: 1 <= i2 by A36, MATRIX_0:32;
A39: i2 <= width (Gauge (C,n)) by A36, MATRIX_0:32;
then A40: i2 <= len (Gauge (C,n)) by JORDAN8:def 1;
consider j1, j2 being Nat such that
A41: [j1,j2] in Indices (Gauge (C,n)) and
A42: (Cage (C,n)) /. i = (Gauge (C,n)) * (j1,j2) by A11, A13, GOBOARD1:def 9;
A43: ( 1 <= j2 & j2 <= width (Gauge (C,n)) ) by A41, MATRIX_0:32;

now :: thesis:

assume ((Cage (C,n)) /. i) `1 = ((Cage (C,n)) /. (i + 1)) `1 ; :: thesis:
then A44: (Cage (C,n)) /. i = (Cage (C,n)) /. (i + 1) by A14, A12, TOPREAL3:6;
then A45: i1 = j1 by A36, A37, A41, A42, GOBOARD1:5;
A46: i2 = j2 by A36, A37, A41, A42, A44, GOBOARD1:5;
|.(j1 - i1).| + |.(j2 - i2).| = 1 by A11, A13, A9, A36, A37, A41, A42, GOBOARD1:def 9;
then 1 = 0 + |.(i2 - j2).| by A45, A46, GOBOARD7:2
.= 0 + 0 by A46, GOBOARD7:2 ;
hence contradiction ; :: thesis:

end;

then A47: ((Cage (C,n)) /. (i + 1)) `1 < ((Cage (C,n)) /. i) `1 by A35, XXREAL_0:1;
((Cage (C,n)) /. (i + 1)) `1 <= p `1 by A5, A8, A35, TOPREAL1:3;
then A48: ((Cage (C,n)) /. (i + 1)) `1 < x `1 by A15, A10, Th77, XXREAL_0:2;
A49: 1 <= i1 by A36, MATRIX_0:32;
A50: i1 <= len (Gauge (C,n)) by A36, MATRIX_0:32;
A51: x `1 = (W-min C) `1 by A1, PSCOMP_1:31
.= W-bound C by EUCLID:52
.= ((Gauge (C,n)) * (2,i2)) `1 by A38, A40, JORDAN8:11 ;
then i1 < 1 + 1 by A48, A37, A38, A39, A50, SPRECT_3:13;
then A52: i1 <= 1 by NAT_1:13;
A53: j1 <= len (Gauge (C,n)) by A41, MATRIX_0:32;
1 <= j1 by A41, MATRIX_0:32;
then i1 < j1 by A37, A38, A39, A50, A42, A43, A47, Th18;
then 1 < j1 by A49, A52, XXREAL_0:1;
then 1 + 1 <= j1 by NAT_1:13;
then x `1 <= ((Cage (C,n)) /. i) `1 by A38, A39, A51, A42, A43, A53, Th18;
then x in L~ (Cage (C,n)) by A8, A14, A12, A48, GOBOARD7:8, SPPOL_2:17;
then x in (L~ (Cage (C,n))) /\ C by A15, XBOOLE_0:def 4;
then L~ (Cage (C,n)) meets C ;
hence contradiction by JORDAN10:5; :: thesis:

end;

end;