let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for k being Element of NAT st 1 <= k & k + 1 <= len (Cage C,n) & (Cage C,n) /. k = W-min (L~ (Cage C,n)) holds
((Cage C,n) /. (k + 1)) `1 = W-bound (L~ (Cage C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for k being Element of NAT st 1 <= k & k + 1 <= len (Cage C,n) & (Cage C,n) /. k = W-min (L~ (Cage C,n)) holds
((Cage C,n) /. (k + 1)) `1 = W-bound (L~ (Cage C,n))
A1: Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
A2: (Cage C,n) /. 1 = N-min (L~ (Cage C,n)) by JORDAN9:34;
then 1 < (N-max (L~ (Cage C,n))) .. (Cage C,n) by SPRECT_2:73;
then 1 < (E-max (L~ (Cage C,n))) .. (Cage C,n) by A2, SPRECT_2:74, XXREAL_0:2;
then 1 < (E-min (L~ (Cage C,n))) .. (Cage C,n) by A2, SPRECT_2:75, XXREAL_0:2;
then 1 < (S-max (L~ (Cage C,n))) .. (Cage C,n) by A2, SPRECT_2:76, XXREAL_0:2;
then 1 < (S-min (L~ (Cage C,n))) .. (Cage C,n) by A2, SPRECT_2:77, XXREAL_0:2;
then A3: (W-min (L~ (Cage C,n))) .. (Cage C,n) > 1 by A2, SPRECT_2:78, XXREAL_0:2;
let k be Element of NAT ; :: thesis: ( 1 <= k & k + 1 <= len (Cage C,n) & (Cage C,n) /. k = W-min (L~ (Cage C,n)) implies ((Cage C,n) /. (k + 1)) `1 = W-bound (L~ (Cage C,n)) )
assume that
A4: 1 <= k and
A5: k + 1 <= len (Cage C,n) and
A6: (Cage C,n) /. k = W-min (L~ (Cage C,n)) ; :: thesis: ((Cage C,n) /. (k + 1)) `1 = W-bound (L~ (Cage C,n))
A7: k < len (Cage C,n) by A5, NAT_1:13;
then A8: k in dom (Cage C,n) by A4, FINSEQ_3:27;
then reconsider k9 = k - 1 as Element of NAT by FINSEQ_3:28;
(W-min (L~ (Cage C,n))) .. (Cage C,n) <= k by A6, A8, FINSEQ_5:42;
then A9: k > 1 by A3, XXREAL_0:2;
then consider i1, j1, i2, j2 being Element of NAT such that
A10: [i1,j1] in Indices (Gauge C,n) and
A11: (Cage C,n) /. k = (Gauge C,n) * i1,j1 and
A12: [i2,j2] in Indices (Gauge C,n) and
A13: (Cage C,n) /. (k + 1) = (Gauge C,n) * i2,j2 and
A14: ( ( 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, A5, JORDAN8:6;
A15: i1 <= len (Gauge C,n) by A10, MATRIX_1:39;
A16: j2 <= width (Gauge C,n) by A12, MATRIX_1:39;
A17: 1 <= i2 by A12, MATRIX_1:39;
A18: j1 <= width (Gauge C,n) by A10, MATRIX_1:39;
A19: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
A20: ( i2 <= len (Gauge C,n) & 1 <= j2 ) by A12, MATRIX_1:39;
A21: k9 + 1 = k ;
A22: k9 + 1 < len (Cage C,n) by A5, NAT_1:13;
A23: 1 <= j1 by A10, MATRIX_1:39;
((Gauge C,n) * i1,j1) `1 = W-bound (L~ (Cage C,n)) by A6, A11, EUCLID:56
.= ((Gauge C,n) * 1,j1) `1 by A23, A18, A19, JORDAN1A:94 ;
then A24: i1 <= 1 by A15, A23, A18, GOBOARD5:4;
k >= 1 + 1 by A9, NAT_1:13;
then A25: k9 >= (1 + 1) - 1 by XREAL_1:11;
then consider i3, j3, i4, j4 being Element of NAT such that
A26: [i3,j3] in Indices (Gauge C,n) and
A27: (Cage C,n) /. k9 = (Gauge C,n) * i3,j3 and
A28: [i4,j4] in Indices (Gauge C,n) and
A29: (Cage C,n) /. (k9 + 1) = (Gauge C,n) * i4,j4 and
A30: ( ( 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, A7, JORDAN8:6;
A31: i1 = i4 by A10, A11, A28, A29, GOBOARD1:21;
A32: j1 = j4 by A10, A11, A28, A29, GOBOARD1:21;
A33: j3 <= width (Gauge C,n) by A26, MATRIX_1:39;
A34: 1 <= j3 by A26, MATRIX_1:39;
A35: 1 <= i1 by A10, MATRIX_1:39;
then A36: i1 = 1 by A24, XXREAL_0:1;
A37: j3 = j4

proof

assume A38: j3 <> j4 ; :: thesis: contradiction

per cases ( ( i3 = i4 & j3 = j4 + 1 ) or ( i3 = i4 & j3 + 1 = j4 ) ) by A30, A38;

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

hence contradiction by A7, A24, A25, A26, A27, A28, A29, A31, JORDAN10:2; :: thesis: verum

end;

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

k9 < len (Cage C,n) by A22, NAT_1:13;
then (Gauge C,n) * i3,j3 in W-most (L~ (Cage C,n)) by A36, A25, A27, A31, A34, A33, A39, JORDAN1A:80;
then A40: ((Gauge C,n) * i3,(j3 + 1)) `2 <= ((Gauge C,n) * i3,j3) `2 by A6, A29, A39, PSCOMP_1:88;
j3 < j3 + 1 by NAT_1:13;
hence contradiction by A35, A15, A18, A31, A32, A34, A39, A40, GOBOARD5:5; :: thesis: verum

end;

end;

end;

A41: 1 <= i3 by A26, MATRIX_1:39;
i1 = i2

proof

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

per cases ( ( i1 = i2 + 1 & j1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) ) by A14, A42;

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

hence contradiction by A17, A24, NAT_1:13; :: thesis: verum

end;

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

k9 + (1 + 1) <= len (Cage C,n) by A5;
then A44: (LSeg (Cage C,n),k9) /\ (LSeg (Cage C,n),k) = {((Cage C,n) /. k)} by A25, A21, TOPREAL1:def 8;
( (Cage C,n) /. k9 in LSeg (Cage C,n),k9 & (Cage C,n) /. (k + 1) in LSeg (Cage C,n),k ) by A4, A5, A7, A25, A21, TOPREAL1:27;
then (Cage C,n) /. (k + 1) in {((Cage C,n) /. k)} by A13, A24, A27, A30, A31, A32, A41, A37, 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 A10, A11, A12, A13, A42, GOBOARD1:21; :: thesis: verum

end;

end;

end;

then ((Gauge C,n) * i1,j1) `1 = ((Gauge C,n) * i2,1) `1 by A35, A15, A23, A18, GOBOARD5:3
.= ((Gauge C,n) * i2,j2) `1 by A17, A20, A16, GOBOARD5:3 ;
hence ((Cage C,n) /. (k + 1)) `1 = W-bound (L~ (Cage C,n)) by A6, A11, A13, EUCLID:56; :: thesis: verum