let n be Nat; :: thesis:
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
A2: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
A3: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;
then 1 < (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:69;
then A4: (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A3, SPRECT_2:70, XXREAL_0:2;
let k be Nat; :: thesis:
assume that
A5: 1 <= k and
A6: k + 1 <= len (Cage (C,n)) and
A7: (Cage (C,n)) /. k = E-max (L~ (Cage (C,n))) ; :: thesis:
A8: k < len (Cage (C,n)) by A6, NAT_1:13;
then A9: k in dom (Cage (C,n)) by A5, FINSEQ_3:25;
then reconsider k9 = k - 1 as Nat by FINSEQ_3:26;
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= k by A7, A9, FINSEQ_5:39;
then A10: k > 1 by A4, XXREAL_0:2;
then consider i1, j1, i2, j2 being Nat such that
A11: [i1,j1] in Indices (Gauge (C,n)) and
A12: (Cage (C,n)) /. k = (Gauge (C,n)) * (i1,j1) and
A13: [i2,j2] in Indices (Gauge (C,n)) and
A14: (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i2,j2) and
A15: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A6, JORDAN8:3;
A16: 1 <= i1 by A11, MATRIX_0:32;
A17: k9 + 1 < len (Cage (C,n)) by A6, NAT_1:13;
A18: 1 <= j1 by A11, MATRIX_0:32;
A19: j2 <= width (Gauge (C,n)) by A13, MATRIX_0:32;
A20: i2 <= len (Gauge (C,n)) by A13, MATRIX_0:32;
A21: j1 <= width (Gauge (C,n)) by A11, MATRIX_0:32;
((Gauge (C,n)) * (i1,j1)) `1 = E-bound (L~ (Cage (C,n))) by A7, A12, EUCLID:52
.= ((Gauge (C,n)) * ((len (Gauge (C,n))),j1)) `1 by A18, A21, A2, JORDAN1A:71 ;
then A22: i1 >= len (Gauge (C,n)) by A16, A18, A21, GOBOARD5:3;
k >= 1 + 1 by A10, NAT_1:13;
then A23: k9 >= (1 + 1) - 1 by XREAL_1:9;
then consider i3, j3, i4, j4 being Nat such that
A24: [i3,j3] in Indices (Gauge (C,n)) and
A25: (Cage (C,n)) /. k9 = (Gauge (C,n)) * (i3,j3) and
A26: [i4,j4] in Indices (Gauge (C,n)) and
A27: (Cage (C,n)) /. (k9 + 1) = (Gauge (C,n)) * (i4,j4) and
A28: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, A8, JORDAN8:3;
A29: i1 = i4 by A11, A12, A26, A27, GOBOARD1:5;
A30: j1 = j4 by A11, A12, A26, A27, GOBOARD1:5;
A31: 1 <= j3 by A24, MATRIX_0:32;
A32: j3 <= width (Gauge (C,n)) by A24, MATRIX_0:32;
A33: i1 <= len (Gauge (C,n)) by A11, MATRIX_0:32;
then A34: i1 = len (Gauge (C,n)) by A22, XXREAL_0:1;
A35: j3 = j4

proof

assume A36: j3 <> j4 ; :: thesis:

per cases by A28, A36;

suppose ( i3 = i4 & j3 + 1 = j4 ) ; :: thesis:

hence contradiction by A8, A22, A23, A24, A25, A26, A27, A29, JORDAN10:1; :: thesis:

end;

suppose A37: ( i3 = i4 & j3 = j4 + 1 ) ; :: thesis:

k9 < len (Cage (C,n)) by A17, NAT_1:13;
then (Gauge (C,n)) * (i3,j3) in E-most (L~ (Cage (C,n))) by A34, A23, A25, A29, A31, A32, A37, JORDAN1A:61;
then A38: ((Gauge (C,n)) * (i4,(j4 + 1))) `2 <= ((Gauge (C,n)) * (i4,j4)) `2 by A7, A27, A37, PSCOMP_1:47;
j4 < j4 + 1 by NAT_1:13;
hence contradiction by A16, A33, A18, A29, A30, A32, A37, A38, GOBOARD5:4; :: thesis:

end;

A39: ( 1 <= i2 & 1 <= j2 ) by A13, MATRIX_0:32;
A40: k9 + 1 = k ;
A41: i3 <= len (Gauge (C,n)) by A24, MATRIX_0:32;
i1 = i2

proof

assume A42: i1 <> i2 ; :: thesis:

per cases by A15, A42;

suppose ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

hence contradiction by A20, A22, NAT_1:13; :: thesis:

end;

suppose A43: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

k9 + (1 + 1) <= len (Cage (C,n)) by A6;
then A44: (LSeg ((Cage (C,n)),k9)) /\ (LSeg ((Cage (C,n)),k)) = {((Cage (C,n)) /. k)} by A23, A40, TOPREAL1:def 6;
( (Cage (C,n)) /. k9 in LSeg ((Cage (C,n)),k9) & (Cage (C,n)) /. (k + 1) in LSeg ((Cage (C,n)),k) ) by A5, A6, A8, A23, A40, TOPREAL1:21;
then (Cage (C,n)) /. (k + 1) in {((Cage (C,n)) /. k)} by A14, A22, A25, A28, A29, A30, A41, A35, A43, A44, NAT_1:13, XBOOLE_0:def 4;
then (Cage (C,n)) /. (k + 1) = (Cage (C,n)) /. k by TARSKI:def 1;
hence contradiction by A11, A12, A13, A14, A42, GOBOARD1:5; :: thesis:

end;

then ((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * (i2,1)) `1 by A16, A33, A18, A21, GOBOARD5:2
.= ((Gauge (C,n)) * (i2,j2)) `1 by A20, A39, A19, GOBOARD5:2 ;
hence ((Cage (C,n)) /. (k + 1)) `1 = E-bound (L~ (Cage (C,n))) by A7, A12, A14, EUCLID:52; :: thesis: