let n be Element of 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 Element of NAT such that
A1: ( 1 <= j & j <= width (Gauge C,n) & W-min (L~ (Cage C,n)) = (Gauge C,n) * 1,j ) by JORDAN1D:34;
set k = (W-min (L~ (Cage C,n))) .. (Cage C,n);
set p = W-min C;
A2: Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
A3: len (Gauge C,n) >= 4 by JORDAN8:13;
then A4: 1 <= len (Gauge C,n) by XXREAL_0:2;
A5: 1 <= (W-min (L~ (Cage C,n))) .. (Cage C,n) by Th3;
A6: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
then A7: (W-min (L~ (Cage C,n))) .. (Cage C,n) <= len (Cage C,n) by FINSEQ_4:31;
A8: (W-min (L~ (Cage C,n))) .. (Cage C,n) in dom (Cage C,n) by A6, FINSEQ_4:30;
A9: (Cage C,n) . ((W-min (L~ (Cage C,n))) .. (Cage C,n)) = W-min (L~ (Cage C,n)) by A6, FINSEQ_4:29;
then A10: (Cage C,n) /. ((W-min (L~ (Cage C,n))) .. (Cage C,n)) = W-min (L~ (Cage C,n)) by A8, PARTFUN1:def 8;
A11: (Cage C,n) /. ((W-min (L~ (Cage C,n))) .. (Cage C,n)) = (Gauge C,n) * 1,j by A1, A8, A9, PARTFUN1:def 8;

now

assume (W-min (L~ (Cage C,n))) .. (Cage C,n) = len (Cage C,n) ; :: thesis:
then A12: (Cage C,n) /. 1 = W-min (L~ (Cage C,n)) by A10, FINSEQ_6:def 1;
A13: 1 in dom (Cage C,n) by A6, FINSEQ_3:33;
A14: 1 < (W-min (L~ (Cage C,n))) .. (Cage C,n) by Th3;
(Cage C,n) . 1 = W-min (L~ (Cage C,n)) by A12, A13, PARTFUN1:def 8;
hence contradiction by A13, A14, FINSEQ_4:34; :: thesis:

end;

then (W-min (L~ (Cage C,n))) .. (Cage C,n) < len (Cage C,n) by A7, XXREAL_0:1;
then A15: ((W-min (L~ (Cage C,n))) .. (Cage C,n)) + 1 <= len (Cage C,n) by NAT_1:13;
then A16: ((Cage C,n) /. (((W-min (L~ (Cage C,n))) .. (Cage C,n)) + 1)) `1 = W-bound (L~ (Cage C,n)) by A5, A10, JORDAN1E:26;
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 A15, FINSEQ_3:27;
then consider ki, kj being Element of NAT such that
A19: ( [ki,kj] in Indices (Gauge C,n) & (Cage C,n) /. (((W-min (L~ (Cage C,n))) .. (Cage C,n)) + 1) = (Gauge C,n) * ki,kj ) by A2, GOBOARD1:def 11;
A20: [1,j] in Indices (Gauge C,n) by A1, A4, MATRIX_1:37;
((Gauge C,n) * 1,j) `1 = ((Gauge C,n) * ki,kj) `1 by A1, A16, A19, EUCLID:56;
then A21: ki = 1 by A19, A20, JORDAN1G:7;
2 <= len (Cage C,n) by GOBOARD7:36, 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 A16, A18, GOBOARD1:16, SPRECT_2:16;
then A22: ((Gauge C,n) * 1,j) `2 <= ((Gauge C,n) * ki,kj) `2 by A1, A19, PSCOMP_1:88;
( 1 <= kj & j <= width (Gauge C,n) & 1 <= ki & ki <= len (Gauge C,n) ) by A1, A19, MATRIX_1:39;
then A23: j <= kj by A21, A22, GOBOARD5:5;
( (W-min (L~ (Cage C,n))) .. (Cage C,n) in dom (Cage C,n) & ((W-min (L~ (Cage C,n))) .. (Cage C,n)) + 1 in dom (Cage C,n) & [1,j] in Indices (GoB (Cage C,n)) & [ki,kj] in Indices (GoB (Cage C,n)) & (Cage C,n) /. ((W-min (L~ (Cage C,n))) .. (Cage C,n)) = (GoB (Cage C,n)) * 1,j & (Cage C,n) /. (((W-min (L~ (Cage C,n))) .. (Cage C,n)) + 1) = (GoB (Cage C,n)) * ki,kj ) by A6, A11, A15, A17, A19, A20, FINSEQ_3:27, FINSEQ_4:30, JORDAN1H:52;
then (abs (1 - ki)) + (abs (j - kj)) = 1 by GOBOARD5:13;
then A24: 0 + (abs (j - kj)) = 1 by A21, ABSVALUE:7;
then A25: kj = j + 1 by A23, GOBOARD1:1;
A26: (Cage C,n) /. (((W-min (L~ (Cage C,n))) .. (Cage C,n)) + 1) = (Gauge C,n) * 1,(j + 1) by A19, A21, A23, A24, GOBOARD1:1;
( 1 <= len (Gauge C,n) & 1 <= j + 1 & j + 1 <= width (Gauge C,n) ) by A3, A19, A25, MATRIX_1:39, XXREAL_0:2;
then [1,(j + 1)] in Indices (Gauge C,n) by MATRIX_1:37;
then A27: right_cell (Cage C,n),((W-min (L~ (Cage C,n))) .. (Cage C,n)),(Gauge C,n) = cell (Gauge C,n),1,j by A1, A2, A5, A10, A15, A20, A26, GOBRD13:23;
A28: GoB (Cage C,n) = Gauge C,n by JORDAN1H:52;

now

assume A29: not W-min C in right_cell (Cage C,n),((W-min (L~ (Cage C,n))) .. (Cage C,n)),(Gauge C,n) ; :: thesis:
A30: 1 < len (Gauge C,n) by A3, XXREAL_0:2;
j + 1 <= width (Gauge C,n) by A19, A25, MATRIX_1:39;
then j < width (Gauge C,n) by NAT_1:13;
then LSeg ((Gauge C,n) * (1 + 1),j),((Gauge C,n) * (1 + 1),(j + 1)) c= cell (Gauge C,n),1,j by A1, A30, GOBOARD5:19;
then A31: not W-min C in LSeg ((Gauge C,n) * 2,j),((Gauge C,n) * 2,(j + 1)) by A27, A29;
( 1 <= j & j <= len (Gauge C,n) ) by A1, JORDAN8:def 1;
then A32: ((Gauge C,n) * 2,j) `1 = W-bound C by JORDAN8:14;
len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
then ( 1 <= j + 1 & j + 1 <= len (Gauge C,n) ) by A19, A25, MATRIX_1:39;
then A33: ((Gauge C,n) * 2,(j + 1)) `1 = W-bound C by JORDAN8:14;
(W-min C) `1 = W-bound C by EUCLID:56;
then A34: ( (W-min C) `2 > ((Gauge C,n) * 2,(j + 1)) `2 or (W-min C) `2 < ((Gauge C,n) * 2,j) `2 ) by A31, A32, A33, GOBOARD7:8;
A35: ( 1 <= j + 1 & j + 1 <= width (Gauge C,n) & 2 <= len (Gauge C,n) ) by A3, A19, A25, MATRIX_1:39, XXREAL_0:2;

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

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

cell (Gauge C,n),1,j meets C by A5, A15, A27, JORDAN9:33;
then (cell (Gauge C,n),1,j) /\ C <> {} by XBOOLE_0:def 7;
then consider c being set such that
A37: c in (cell (Gauge C,n),1,j) /\ C by XBOOLE_0:def 1;
reconsider c = c as Element of (TOP-REAL 2) by A37;
A38: ( c in cell (Gauge C,n),1,j & c in C ) by A37, XBOOLE_0:def 4;
then A39: c `1 >= W-bound C by PSCOMP_1:71;
( 1 + 1 <= len (Gauge C,n) & 1 <= j & j + 1 <= width (Gauge C,n) ) by A1, A3, A19, A25, MATRIX_1:39, XXREAL_0:2;
then A40: ( ((Gauge C,n) * 1,j) `1 <= c `1 & c `1 <= ((Gauge C,n) * (1 + 1),j) `1 & ((Gauge C,n) * 1,j) `2 <= c `2 & c `2 <= ((Gauge C,n) * 1,(j + 1)) `2 ) by A38, JORDAN9:19;
then c in W-most C by A32, A38, A39, SPRECT_2:16, XXREAL_0:1;
then c `2 >= (W-min C) `2 by PSCOMP_1:88;
hence contradiction by A36, A40, XXREAL_0:2; :: thesis:

end;

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

W-min C in C by SPRECT_1:15;
then west_halfline (W-min C) meets L~ (Cage C,n) by JORDAN1A:75;
then consider r being set such that
A42: ( r in west_halfline (W-min C) & r in L~ (Cage C,n) ) by XBOOLE_0:3;
reconsider r = r as Element of (TOP-REAL 2) by A42;
A43: W-min C in W-most C by PSCOMP_1:91;
r in (west_halfline (W-min C)) /\ (L~ (Cage C,n)) by A42, XBOOLE_0:def 4;
then r `1 = W-bound (L~ (Cage C,n)) by A43, JORDAN1A:106;
then r in W-most (L~ (Cage C,n)) by A42, SPRECT_2:16;
then (W-min (L~ (Cage C,n))) `2 <= r `2 by PSCOMP_1:88;
hence contradiction by A1, A41, A42, TOPREAL1:def 15; :: thesis:

end;

then W-min C in right_cell (Cage C,n),((W-min (L~ (Cage C,n))) .. (Cage C,n)) by A5, A15, A28, JORDAN1H:29;
hence W-min C in right_cell (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))),1 by A6, Th7; :: thesis: