let n be Nat; :: thesis:
let C be non empty connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
set f = Cage (C,n);
set G = Gauge (C,n);
consider j being Nat such that
A1: 1 <= j and
A2: j <= width (Gauge (C,n)) and
A3: W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,j) by JORDAN1D:30;
A4: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A5: 1 <= len (Gauge (C,n)) by XXREAL_0:2;
set k = (W-min (L~ (Cage (C,n)))) .. (Cage (C,n));
A6: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
then A7: ( (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) in dom (Cage (C,n)) & (Cage (C,n)) . ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = W-min (L~ (Cage (C,n))) ) by FINSEQ_4:19, FINSEQ_4:20;
then A8: (Cage (C,n)) /. ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = W-min (L~ (Cage (C,n))) by PARTFUN1:def 6;

A9: now :: thesis:

A10: 1 < (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th1;
A11: 1 in dom (Cage (C,n)) by A6, FINSEQ_3:31;
assume (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) = len (Cage (C,n)) ; :: thesis:
then (Cage (C,n)) /. 1 = W-min (L~ (Cage (C,n))) by A8, FINSEQ_6:def 1;
then (Cage (C,n)) . 1 = W-min (L~ (Cage (C,n))) by A11, PARTFUN1:def 6;
hence contradiction by A11, A10, FINSEQ_4:24; :: thesis:

end;

1 <= len (Gauge (C,n)) by A4, XXREAL_0:2;
then A12: [1,j] in Indices (Gauge (C,n)) by A1, A2, MATRIX_0:30;
then A13: [1,j] in Indices (GoB (Cage (C,n))) by JORDAN1H:44;
(W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= len (Cage (C,n)) by A6, FINSEQ_4:21;
then (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by A9, XXREAL_0:1;
then A14: ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13;
(Cage (C,n)) /. ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * (1,j) by A3, A7, PARTFUN1:def 6;
then A15: (Cage (C,n)) /. ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) = (GoB (Cage (C,n))) * (1,j) by JORDAN1H:44;
set p = W-min C;
A16: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
A17: 1 <= ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 by NAT_1:11;
then A18: ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A14, FINSEQ_3:25;
A19: ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A14, A17, FINSEQ_3:25;
then consider ki, kj being Nat such that
A20: [ki,kj] in Indices (Gauge (C,n)) and
A21: (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * (ki,kj) by A16, GOBOARD1:def 9;
A22: ( 1 <= kj & ki <= len (Gauge (C,n)) ) by A20, MATRIX_0:32;
A23: 1 <= (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th1;
then A24: ((Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1)) `1 = W-bound (L~ (Cage (C,n))) by A8, A14, JORDAN1E:22;
then ((Gauge (C,n)) * (1,j)) `1 = ((Gauge (C,n)) * (ki,kj)) `1 by A3, A21, EUCLID:52;
then A25: ki = 1 by A20, A12, JORDAN1G:7;
2 <= len (Cage (C,n)) by GOBOARD7:34, XXREAL_0:2;
then (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) in W-most (L~ (Cage (C,n))) by A24, A19, GOBOARD1:1, SPRECT_2:12;
then ((Gauge (C,n)) * (1,j)) `2 <= ((Gauge (C,n)) * (ki,kj)) `2 by A3, A21, PSCOMP_1:31;
then A26: j <= kj by A2, A25, A22, GOBOARD5:4;
( [ki,kj] in Indices (GoB (Cage (C,n))) & (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (GoB (Cage (C,n))) * (ki,kj) ) by A20, A21, JORDAN1H:44;
then |.(1 - ki).| + |.(j - kj).| = 1 by A6, A18, A13, A15, FINSEQ_4:20, GOBOARD5:12;
then A27: 0 + |.(j - kj).| = 1 by A25, ABSVALUE:2;
then A28: (Cage (C,n)) /. (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1) = (Gauge (C,n)) * (1,(j + 1)) by A21, A25, A26, SEQM_3:41;
A29: kj = j + 1 by A26, A27, SEQM_3:41;
then ( 1 <= j + 1 & j + 1 <= width (Gauge (C,n)) ) by A20, MATRIX_0:32;
then [1,(j + 1)] in Indices (Gauge (C,n)) by A5, MATRIX_0:30;
then A30: right_cell ((Cage (C,n)),((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) = cell ((Gauge (C,n)),1,j) by A3, A16, A23, A8, A14, A12, A28, GOBRD13:22;

A31: now :: thesis:

len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
then A32: j + 1 <= len (Gauge (C,n)) by A20, A29, MATRIX_0:32;
1 <= j + 1 by A20, A29, MATRIX_0:32;
then A33: ((Gauge (C,n)) * (2,(j + 1))) `1 = W-bound C by A32, JORDAN8:11;
assume A34: not W-min C in right_cell ((Cage (C,n)),((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))),(Gauge (C,n))) ; :: thesis:
j + 1 <= width (Gauge (C,n)) by A20, A29, MATRIX_0:32;
then A35: j < width (Gauge (C,n)) by NAT_1:13;
A36: 2 <= len (Gauge (C,n)) by A4, XXREAL_0:2;
1 < len (Gauge (C,n)) by A4, XXREAL_0:2;
then LSeg (((Gauge (C,n)) * ((1 + 1),j)),((Gauge (C,n)) * ((1 + 1),(j + 1)))) c= cell ((Gauge (C,n)),1,j) by A1, A35, GOBOARD5:18;
then A37: not W-min C in LSeg (((Gauge (C,n)) * (2,j)),((Gauge (C,n)) * (2,(j + 1)))) by A30, A34;
A38: ( 1 <= j + 1 & j + 1 <= width (Gauge (C,n)) ) by A20, A29, MATRIX_0:32;
j <= len (Gauge (C,n)) by A2, JORDAN8:def 1;
then A39: ((Gauge (C,n)) * (2,j)) `1 = W-bound C by A1, JORDAN8:11;
(W-min C) `1 = W-bound C by EUCLID:52;
then A40: ( (W-min C) `2 > ((Gauge (C,n)) * (2,(j + 1))) `2 or (W-min C) `2 < ((Gauge (C,n)) * (2,j)) `2 ) by A37, A39, A33, GOBOARD7:7;

per cases ) `2 > ((Gauge (C,n)) * (1,(j + 1))) `2 or (W-min C) `2 < ((Gauge (C,n)) * (1,j)) `2 ) by A1, A2, A40, A38, A36, GOBOARD5:1;

suppose A41: (W-min C) `2 > ((Gauge (C,n)) * (1,(j + 1))) `2 ; :: thesis:

cell ((Gauge (C,n)),1,j) meets C by A23, A14, A30, JORDAN9:31;
then (cell ((Gauge (C,n)),1,j)) /\ C <> {} by XBOOLE_0:def 7;
then consider c being object such that
A42: c in (cell ((Gauge (C,n)),1,j)) /\ C by XBOOLE_0:def 1;
reconsider c = c as Element of (TOP-REAL 2) by A42;
A43: c in cell ((Gauge (C,n)),1,j) by A42, XBOOLE_0:def 4;
A44: c in C by A42, XBOOLE_0:def 4;
then A45: c `1 >= W-bound C by PSCOMP_1:24;
A46: ( 1 + 1 <= len (Gauge (C,n)) & j + 1 <= width (Gauge (C,n)) ) by A4, A20, A29, MATRIX_0:32, XXREAL_0:2;
then c `1 <= ((Gauge (C,n)) * ((1 + 1),j)) `1 by A1, A43, JORDAN9:17;
then c in W-most C by A39, A44, A45, SPRECT_2:12, XXREAL_0:1;
then A47: c `2 >= (W-min C) `2 by PSCOMP_1:31;
c `2 <= ((Gauge (C,n)) * (1,(j + 1))) `2 by A1, A43, A46, JORDAN9:17;
hence contradiction by A41, A47, XXREAL_0:2; :: thesis:

end;

suppose A48: (W-min C) `2 < ((Gauge (C,n)) * (1,j)) `2 ; :: thesis:

west_halfline (W-min C) meets L~ (Cage (C,n)) by JORDAN1A:54, SPRECT_1:13;
then consider r being object such that
A49: r in west_halfline (W-min C) and
A50: r in L~ (Cage (C,n)) by XBOOLE_0:3;
reconsider r = r as Element of (TOP-REAL 2) by A49;
r in (west_halfline (W-min C)) /\ (L~ (Cage (C,n))) by A49, A50, XBOOLE_0:def 4;
then r `1 = W-bound (L~ (Cage (C,n))) by JORDAN1A:85, PSCOMP_1:34;
then r in W-most (L~ (Cage (C,n))) by A50, SPRECT_2:12;
then (W-min (L~ (Cage (C,n)))) `2 <= r `2 by PSCOMP_1:31;
hence contradiction by A3, A48, A49, TOPREAL1:def 13; :: thesis:

end;

GoB (Cage (C,n)) = Gauge (C,n) by JORDAN1H:44;
then W-min C in right_cell ((Cage (C,n)),((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) by A23, A14, A31, JORDAN1H:23;
hence W-min C in right_cell ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),1) by A6, Th5; :: thesis: