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 and
A2: j <= width (Gauge C,n) and
A3: W-min (L~ (Cage C,n)) = (Gauge C,n) * 1,j by JORDAN1D:34;
A4: len (Gauge C,n) >= 4 by JORDAN8:13;
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:47;
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:29, FINSEQ_4:30;
then A8: (Cage C,n) /. ((W-min (L~ (Cage C,n))) .. (Cage C,n)) = W-min (L~ (Cage C,n)) by PARTFUN1:def 8;

A9: now

A10: 1 < (W-min (L~ (Cage C,n))) .. (Cage C,n) by Th3;
A11: 1 in dom (Cage C,n) by A6, FINSEQ_3:33;
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 8;
hence contradiction by A11, A10, FINSEQ_4:34; :: 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_1:37;
then A13: [1,j] in Indices (GoB (Cage C,n)) by JORDAN1H:52;
(W-min (L~ (Cage C,n))) .. (Cage C,n) <= len (Cage C,n) by A6, FINSEQ_4:31;
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 8;
then A15: (Cage C,n) /. ((W-min (L~ (Cage C,n))) .. (Cage C,n)) = (GoB (Cage C,n)) * 1,j by JORDAN1H:52;
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:27;
A19: ((W-min (L~ (Cage C,n))) .. (Cage C,n)) + 1 in dom (Cage C,n) by A14, A17, FINSEQ_3:27;
then consider ki, kj being Element of 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 11;
A22: ( 1 <= kj & ki <= len (Gauge C,n) ) by A20, MATRIX_1:39;
A23: 1 <= (W-min (L~ (Cage C,n))) .. (Cage C,n) by Th3;
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:26;
then ((Gauge C,n) * 1,j) `1 = ((Gauge C,n) * ki,kj) `1 by A3, A21, EUCLID:56;
then A25: ki = 1 by A20, A12, 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 A24, A19, GOBOARD1:16, SPRECT_2:16;
then ((Gauge C,n) * 1,j) `2 <= ((Gauge C,n) * ki,kj) `2 by A3, A21, PSCOMP_1:88;
then A26: j <= kj by A2, A25, A22, GOBOARD5:5;
( [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:52;
then (abs (1 - ki)) + (abs (j - kj)) = 1 by A6, A18, A13, A15, FINSEQ_4:30, GOBOARD5:13;
then A27: 0 + (abs (j - kj)) = 1 by A25, ABSVALUE:7;
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:81;
A29: kj = j + 1 by A26, A27, SEQM_3:81;
then ( 1 <= j + 1 & j + 1 <= width (Gauge C,n) ) by A20, MATRIX_1:39;
then [1,(j + 1)] in Indices (Gauge C,n) by A5, MATRIX_1:37;
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:23;

A31: now

len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
then A32: j + 1 <= len (Gauge C,n) by A20, A29, MATRIX_1:39;
1 <= j + 1 by A20, A29, MATRIX_1:39;
then A33: ((Gauge C,n) * 2,(j + 1)) `1 = W-bound C by A32, JORDAN8:14;
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_1:39;
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:19;
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_1:39;
j <= len (Gauge C,n) by A2, JORDAN8:def 1;
then A39: ((Gauge C,n) * 2,j) `1 = W-bound C by A1, JORDAN8:14;
(W-min C) `1 = W-bound C by EUCLID:56;
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:8;

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

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:33;
then (cell (Gauge C,n),1,j) /\ C <> {} by XBOOLE_0:def 7;
then consider c being set 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:71;
A46: ( 1 + 1 <= len (Gauge C,n) & j + 1 <= width (Gauge C,n) ) by A4, A20, A29, MATRIX_1:39, XXREAL_0:2;
then c `1 <= ((Gauge C,n) * (1 + 1),j) `1 by A1, A43, JORDAN9:19;
then c in W-most C by A39, A44, A45, SPRECT_2:16, XXREAL_0:1;
then A47: c `2 >= (W-min C) `2 by PSCOMP_1:88;
c `2 <= ((Gauge C,n) * 1,(j + 1)) `2 by A1, A43, A46, JORDAN9:19;
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:75, SPRECT_1:15;
then consider r being set 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:106, PSCOMP_1:91;
then r in W-most (L~ (Cage C,n)) by A50, SPRECT_2:16;
then (W-min (L~ (Cage C,n))) `2 <= r `2 by PSCOMP_1:88;
hence contradiction by A3, A48, A49, TOPREAL1:def 15; :: thesis:

end;

end;

end;

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