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) & E-max (L~ (Cage C,n)) = (Gauge C,n) * (len (Gauge C,n)),j ) by JORDAN1D:29;
set k = (E-max (L~ (Cage C,n))) .. (Cage C,n);
set p = E-max 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 <= (E-max (L~ (Cage C,n))) .. (Cage C,n) by Th4;
A6: E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A7: (E-max (L~ (Cage C,n))) .. (Cage C,n) <= len (Cage C,n) by FINSEQ_4:31;
A8: (E-max (L~ (Cage C,n))) .. (Cage C,n) in dom (Cage C,n) by A6, FINSEQ_4:30;
A9: (Cage C,n) . ((E-max (L~ (Cage C,n))) .. (Cage C,n)) = E-max (L~ (Cage C,n)) by A6, FINSEQ_4:29;
then A10: (Cage C,n) /. ((E-max (L~ (Cage C,n))) .. (Cage C,n)) = E-max (L~ (Cage C,n)) by A8, PARTFUN1:def 8;
A11: (Cage C,n) /. ((E-max (L~ (Cage C,n))) .. (Cage C,n)) = (Gauge C,n) * (len (Gauge C,n)),j by A1, A8, A9, PARTFUN1:def 8;
A12: (Cage C,n) /. ((E-max (L~ (Cage C,n))) .. (Cage C,n)) = (Gauge C,n) * (len (Gauge C,n)),((j -' 1) + 1) by A1, A10, XREAL_1:237;

now

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

end;

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

now

assume A29: not E-max C in right_cell (Cage C,n),((E-max (L~ (Cage C,n))) .. (Cage C,n)),(Gauge C,n) ; :: thesis:
A30: 1 < len (Gauge C,n) by A3, XXREAL_0:2;
then A31: 1 <= (len (Gauge C,n)) -' 1 by NAT_D:49;
A32: (len (Gauge C,n)) -' 1 <= len (Gauge C,n) by NAT_D:50;
j -' 1 < j by A26, NAT_D:51;
then j -' 1 < width (Gauge C,n) by A1, XXREAL_0:2;
then LSeg ((Gauge C,n) * ((len (Gauge C,n)) -' 1),(j -' 1)),((Gauge C,n) * ((len (Gauge C,n)) -' 1),((j -' 1) + 1)) c= cell (Gauge C,n),((len (Gauge C,n)) -' 1),(j -' 1) by A26, A31, A32, GOBOARD5:20;
then not E-max C in LSeg ((Gauge C,n) * ((len (Gauge C,n)) -' 1),(j -' 1)),((Gauge C,n) * ((len (Gauge C,n)) -' 1),((j -' 1) + 1)) by A27, A29;
then A33: not E-max C in LSeg ((Gauge C,n) * ((len (Gauge C,n)) -' 1),(j -' 1)),((Gauge C,n) * ((len (Gauge C,n)) -' 1),j) by A1, XREAL_1:237;
( 1 <= j -' 1 & j -' 1 <= len (Gauge C,n) ) by A26, JORDAN8:def 1;
then A34: ((Gauge C,n) * ((len (Gauge C,n)) -' 1),(j -' 1)) `1 = E-bound C by JORDAN8:15;
( 1 <= j & j <= len (Gauge C,n) ) by A1, JORDAN8:def 1;
then A35: ((Gauge C,n) * ((len (Gauge C,n)) -' 1),j) `1 = E-bound C by JORDAN8:15;
(E-max C) `1 = E-bound C by EUCLID:56;
then A36: ( (E-max C) `2 > ((Gauge C,n) * ((len (Gauge C,n)) -' 1),j) `2 or (E-max C) `2 < ((Gauge C,n) * ((len (Gauge C,n)) -' 1),(j -' 1)) `2 ) by A33, A34, A35, GOBOARD7:8;
A37: ((Gauge C,n) * 1,j) `2 = ((Gauge C,n) * ((len (Gauge C,n)) -' 1),j) `2 by A1, A31, A32, GOBOARD5:2;
A38: ((Gauge C,n) * 1,(j -' 1)) `2 = ((Gauge C,n) * ((len (Gauge C,n)) -' 1),(j -' 1)) `2 by A26, A31, A32, GOBOARD5:2;

per cases ) `2 < ((Gauge C,n) * (len (Gauge C,n)),(j -' 1)) `2 or (E-max C) `2 > ((Gauge C,n) * (len (Gauge C,n)),j) `2 ) by A1, A26, A36, A37, A38, GOBOARD5:2;

suppose A39: (E-max C) `2 < ((Gauge C,n) * (len (Gauge C,n)),(j -' 1)) `2 ; :: thesis:

cell (Gauge C,n),((len (Gauge C,n)) -' 1),(j -' 1) meets C by A5, A16, A27, JORDAN9:33;
then (cell (Gauge C,n),((len (Gauge C,n)) -' 1),(j -' 1)) /\ C <> {} by XBOOLE_0:def 7;
then consider c being set such that
A40: c in (cell (Gauge C,n),((len (Gauge C,n)) -' 1),(j -' 1)) /\ C by XBOOLE_0:def 1;
reconsider c = c as Element of (TOP-REAL 2) by A40;
A41: ( c in cell (Gauge C,n),((len (Gauge C,n)) -' 1),(j -' 1) & c in C ) by A40, XBOOLE_0:def 4;
then A42: c `1 <= E-bound C by PSCOMP_1:71;
( 1 <= (len (Gauge C,n)) -' 1 & ((len (Gauge C,n)) -' 1) + 1 <= len (Gauge C,n) & 1 <= j -' 1 & (j -' 1) + 1 <= width (Gauge C,n) ) by A1, A20, A25, A30, MATRIX_1:39, NAT_D:49, XREAL_1:237;
then A43: ( ((Gauge C,n) * ((len (Gauge C,n)) -' 1),(j -' 1)) `1 <= c `1 & c `1 <= ((Gauge C,n) * (((len (Gauge C,n)) -' 1) + 1),(j -' 1)) `1 & ((Gauge C,n) * ((len (Gauge C,n)) -' 1),(j -' 1)) `2 <= c `2 & c `2 <= ((Gauge C,n) * ((len (Gauge C,n)) -' 1),((j -' 1) + 1)) `2 ) by A41, JORDAN9:19;
then ((Gauge C,n) * 1,(j -' 1)) `2 <= c `2 by A26, A31, A32, GOBOARD5:2;
then A44: ((Gauge C,n) * (len (Gauge C,n)),(j -' 1)) `2 <= c `2 by A26, GOBOARD5:2;
c in E-most C by A34, A41, A42, A43, SPRECT_2:17, XXREAL_0:1;
then c `2 <= (E-max C) `2 by PSCOMP_1:108;
hence contradiction by A39, A44, XXREAL_0:2; :: thesis:

end;

suppose A45: (E-max C) `2 > ((Gauge C,n) * (len (Gauge C,n)),j) `2 ; :: thesis:

E-max C in C by SPRECT_1:16;
then east_halfline (E-max C) meets L~ (Cage C,n) by JORDAN1A:73;
then consider r being set such that
A46: ( r in east_halfline (E-max C) & r in L~ (Cage C,n) ) by XBOOLE_0:3;
reconsider r = r as Element of (TOP-REAL 2) by A46;
A47: E-max C in E-most C by PSCOMP_1:111;
r in (east_halfline (E-max C)) /\ (L~ (Cage C,n)) by A46, XBOOLE_0:def 4;
then r `1 = E-bound (L~ (Cage C,n)) by A47, JORDAN1A:104;
then r in E-most (L~ (Cage C,n)) by A46, SPRECT_2:17;
then (E-max (L~ (Cage C,n))) `2 >= r `2 by PSCOMP_1:108;
hence contradiction by A1, A45, A46, TOPREAL1:def 13; :: thesis:

end;

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