let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for k being 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 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:32;

then 1 < (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:69;

then 1 < (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, SPRECT_2:70, XXREAL_0:2;

then 1 < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, SPRECT_2:71, XXREAL_0:2;

then 1 < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, SPRECT_2:72, XXREAL_0:2;

then 1 < (S-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, SPRECT_2:73, XXREAL_0:2;

then A3: (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A2, SPRECT_2:74, XXREAL_0:2;

let k be 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:25;

then reconsider k9 = k - 1 as Nat by FINSEQ_3:26;

(W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= k by A6, A8, FINSEQ_5:39;

then A9: k > 1 by A3, XXREAL_0:2;

then consider i1, j1, i2, j2 being 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:3;

A15: i1 <= len (Gauge (C,n)) by A10, MATRIX_0:32;

A16: j2 <= width (Gauge (C,n)) by A12, MATRIX_0:32;

A17: 1 <= i2 by A12, MATRIX_0:32;

A18: j1 <= width (Gauge (C,n)) by A10, MATRIX_0:32;

A19: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;

A20: ( i2 <= len (Gauge (C,n)) & 1 <= j2 ) by A12, MATRIX_0:32;

A21: k9 + 1 = k ;

A22: k9 + 1 < len (Cage (C,n)) by A5, NAT_1:13;

A23: 1 <= j1 by A10, MATRIX_0:32;

((Gauge (C,n)) * (i1,j1)) `1 = W-bound (L~ (Cage (C,n))) by A6, A11, EUCLID:52

.= ((Gauge (C,n)) * (1,j1)) `1 by A23, A18, A19, JORDAN1A:73 ;

then A24: i1 <= 1 by A15, A23, A18, GOBOARD5:3;

k >= 1 + 1 by A9, NAT_1:13;

then A25: k9 >= (1 + 1) - 1 by XREAL_1:9;

then consider i3, j3, i4, j4 being 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:3;

A31: i1 = i4 by A10, A11, A28, A29, GOBOARD1:5;

A32: j1 = j4 by A10, A11, A28, A29, GOBOARD1:5;

A33: j3 <= width (Gauge (C,n)) by A26, MATRIX_0:32;

A34: 1 <= j3 by A26, MATRIX_0:32;

A35: 1 <= i1 by A10, MATRIX_0:32;

then A36: i1 = 1 by A24, XXREAL_0:1;

A37: j3 = j4

i1 = i2

.= ((Gauge (C,n)) * (i2,j2)) `1 by A17, A20, A16, GOBOARD5:2 ;

hence ((Cage (C,n)) /. (k + 1)) `1 = W-bound (L~ (Cage (C,n))) by A6, A11, A13, EUCLID:52; :: thesis: verum

for k being 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 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:32;

then 1 < (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:69;

then 1 < (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, SPRECT_2:70, XXREAL_0:2;

then 1 < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, SPRECT_2:71, XXREAL_0:2;

then 1 < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, SPRECT_2:72, XXREAL_0:2;

then 1 < (S-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, SPRECT_2:73, XXREAL_0:2;

then A3: (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A2, SPRECT_2:74, XXREAL_0:2;

let k be 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:25;

then reconsider k9 = k - 1 as Nat by FINSEQ_3:26;

(W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= k by A6, A8, FINSEQ_5:39;

then A9: k > 1 by A3, XXREAL_0:2;

then consider i1, j1, i2, j2 being 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:3;

A15: i1 <= len (Gauge (C,n)) by A10, MATRIX_0:32;

A16: j2 <= width (Gauge (C,n)) by A12, MATRIX_0:32;

A17: 1 <= i2 by A12, MATRIX_0:32;

A18: j1 <= width (Gauge (C,n)) by A10, MATRIX_0:32;

A19: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;

A20: ( i2 <= len (Gauge (C,n)) & 1 <= j2 ) by A12, MATRIX_0:32;

A21: k9 + 1 = k ;

A22: k9 + 1 < len (Cage (C,n)) by A5, NAT_1:13;

A23: 1 <= j1 by A10, MATRIX_0:32;

((Gauge (C,n)) * (i1,j1)) `1 = W-bound (L~ (Cage (C,n))) by A6, A11, EUCLID:52

.= ((Gauge (C,n)) * (1,j1)) `1 by A23, A18, A19, JORDAN1A:73 ;

then A24: i1 <= 1 by A15, A23, A18, GOBOARD5:3;

k >= 1 + 1 by A9, NAT_1:13;

then A25: k9 >= (1 + 1) - 1 by XREAL_1:9;

then consider i3, j3, i4, j4 being 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:3;

A31: i1 = i4 by A10, A11, A28, A29, GOBOARD1:5;

A32: j1 = j4 by A10, A11, A28, A29, GOBOARD1:5;

A33: j3 <= width (Gauge (C,n)) by A26, MATRIX_0:32;

A34: 1 <= j3 by A26, MATRIX_0:32;

A35: 1 <= i1 by A10, MATRIX_0:32;

then A36: i1 = 1 by A24, XXREAL_0:1;

A37: j3 = j4

proof

A41:
1 <= i3
by A26, MATRIX_0:32;
assume A38:
j3 <> j4
; :: thesis: contradiction

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

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:59;

then A40: ((Gauge (C,n)) * (i3,(j3 + 1))) `2 <= ((Gauge (C,n)) * (i3,j3)) `2 by A6, A29, A39, PSCOMP_1:31;

j3 < j3 + 1 by NAT_1:13;

hence contradiction by A35, A15, A18, A31, A32, A34, A39, A40, GOBOARD5:4; :: thesis: verum

end;then (Gauge (C,n)) * (i3,j3) in W-most (L~ (Cage (C,n))) by A36, A25, A27, A31, A34, A33, A39, JORDAN1A:59;

then A40: ((Gauge (C,n)) * (i3,(j3 + 1))) `2 <= ((Gauge (C,n)) * (i3,j3)) `2 by A6, A29, A39, PSCOMP_1:31;

j3 < j3 + 1 by NAT_1:13;

hence contradiction by A35, A15, A18, A31, A32, A34, A39, A40, GOBOARD5:4; :: thesis: verum

i1 = i2

proof

then ((Gauge (C,n)) * (i1,j1)) `1 =
((Gauge (C,n)) * (i2,1)) `1
by A35, A15, A23, A18, GOBOARD5:2
assume A42:
i1 <> i2
; :: thesis: contradiction

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

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 6;

( (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:21;

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:5; :: thesis: verum

end;then A44: (LSeg ((Cage (C,n)),k9)) /\ (LSeg ((Cage (C,n)),k)) = {((Cage (C,n)) /. k)} by A25, A21, 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 A4, A5, A7, A25, A21, TOPREAL1:21;

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:5; :: thesis: verum

.= ((Gauge (C,n)) * (i2,j2)) `1 by A17, A20, A16, GOBOARD5:2 ;

hence ((Cage (C,n)) /. (k + 1)) `1 = W-bound (L~ (Cage (C,n))) by A6, A11, A13, EUCLID:52; :: thesis: verum