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: E-max (L~ (Cage C,n)) = (Gauge C,n) * (len (Gauge C,n)),j by JORDAN1D:29;
A4: len (Gauge C,n) >= 4 by JORDAN8:13;
then A5: 1 <= len (Gauge C,n) by XXREAL_0:2;
set k = (E-max (L~ (Cage C,n))) .. (Cage C,n);
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) in dom (Cage C,n) & (Cage C,n) . ((E-max (L~ (Cage C,n))) .. (Cage C,n)) = E-max (L~ (Cage C,n)) ) by FINSEQ_4:29, FINSEQ_4:30;
then A8: (Cage C,n) /. ((E-max (L~ (Cage C,n))) .. (Cage C,n)) = E-max (L~ (Cage C,n)) by PARTFUN1:def 8;

A9: now

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

end;

(Cage C,n) /. ((E-max (L~ (Cage C,n))) .. (Cage C,n)) = (Gauge C,n) * (len (Gauge C,n)),j by A3, A7, PARTFUN1:def 8;
then A12: (Cage C,n) /. ((E-max (L~ (Cage C,n))) .. (Cage C,n)) = (GoB (Cage C,n)) * (len (Gauge C,n)),j by JORDAN1H:52;
(E-max (L~ (Cage C,n))) .. (Cage C,n) <= len (Cage C,n) by A6, FINSEQ_4:31;
then (E-max (L~ (Cage C,n))) .. (Cage C,n) < len (Cage C,n) by A9, XXREAL_0:1;
then A13: ((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1 <= len (Cage C,n) by NAT_1:13;
A14: 1 <= len (Gauge C,n) by A4, XXREAL_0:2;
then A15: [(len (Gauge C,n)),j] in Indices (Gauge C,n) by A1, A2, MATRIX_1:37;
( 1 <= (j -' 1) + 1 & (j -' 1) + 1 <= width (Gauge C,n) ) by A1, A2, XREAL_1:237;
then A16: [(len (Gauge C,n)),((j -' 1) + 1)] in Indices (Gauge C,n) by A14, MATRIX_1:37;
set p = E-max C;
A17: Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
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 A13, FINSEQ_3:27;
A20: ((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1 in dom (Cage C,n) by A13, A18, FINSEQ_3:27;
then consider ki, kj being Element of NAT such that
A21: [ki,kj] in Indices (Gauge C,n) and
A22: (Cage C,n) /. (((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) = (Gauge C,n) * ki,kj by A17, GOBOARD1:def 11;
A23: ( [ki,kj] in Indices (GoB (Cage C,n)) & (Cage C,n) /. (((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) = (GoB (Cage C,n)) * ki,kj ) by A21, A22, JORDAN1H:52;
A24: 1 <= (E-max (L~ (Cage C,n))) .. (Cage C,n) by Th4;
then A25: ((Cage C,n) /. (((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1)) `1 = E-bound (L~ (Cage C,n)) by A8, A13, JORDAN1E:24;
then ((Gauge C,n) * (len (Gauge C,n)),j) `1 = ((Gauge C,n) * ki,kj) `1 by A3, A22, EUCLID:56;
then A26: ki = len (Gauge C,n) by A21, A15, JORDAN1G:7;
A27: ( kj <= width (Gauge C,n) & 1 <= ki ) by A21, MATRIX_1:39;
[(len (Gauge C,n)),j] in Indices (GoB (Cage C,n)) by A15, JORDAN1H:52;
then (abs ((len (Gauge C,n)) - ki)) + (abs (j - kj)) = 1 by A6, A19, A12, A23, FINSEQ_4:30, GOBOARD5:13;
then A28: 0 + (abs (j - kj)) = 1 by A26, ABSVALUE: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 A25, A20, GOBOARD1:16, SPRECT_2:17;
then ((Gauge C,n) * (len (Gauge C,n)),j) `2 >= ((Gauge C,n) * ki,kj) `2 by A3, A22, PSCOMP_1:108;
then j >= kj by A1, A26, A27, GOBOARD5:5;
then j = kj + 1 by A28, SEQM_3:81;
then kj = j - 1 ;
then A29: kj = j -' 1 by A1, XREAL_1:235;
then A30: 1 <= j -' 1 by A21, MATRIX_1:39;
A31: j -' 1 <= width (Gauge C,n) by A21, A29, MATRIX_1:39;
(Cage C,n) /. ((E-max (L~ (Cage C,n))) .. (Cage C,n)) = (Gauge C,n) * (len (Gauge C,n)),((j -' 1) + 1) by A1, A3, A8, XREAL_1:237;
then A32: 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 A17, A24, A13, A21, A22, A26, A29, A16, GOBRD13:29;

A33: now

j -' 1 <= len (Gauge C,n) by A31, JORDAN8:def 1;
then A34: ((Gauge C,n) * ((len (Gauge C,n)) -' 1),(j -' 1)) `1 = E-bound C by A30, JORDAN8:15;
j <= len (Gauge C,n) by A2, JORDAN8:def 1;
then A35: ((Gauge C,n) * ((len (Gauge C,n)) -' 1),j) `1 = E-bound C by A1, JORDAN8:15;
assume A36: not E-max C in right_cell (Cage C,n),((E-max (L~ (Cage C,n))) .. (Cage C,n)),(Gauge C,n) ; :: thesis:
A37: 1 < len (Gauge C,n) by A4, XXREAL_0:2;
then A38: 1 <= (len (Gauge C,n)) -' 1 by NAT_D:49;
A39: (len (Gauge C,n)) -' 1 <= len (Gauge C,n) by NAT_D:50;
then A40: ( ((Gauge C,n) * 1,j) `2 = ((Gauge C,n) * ((len (Gauge C,n)) -' 1),j) `2 & ((Gauge C,n) * 1,(j -' 1)) `2 = ((Gauge C,n) * ((len (Gauge C,n)) -' 1),(j -' 1)) `2 ) by A1, A2, A30, A31, A38, GOBOARD5:2;
j -' 1 < j by A30, NAT_D:51;
then j -' 1 < width (Gauge C,n) by A2, 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 A30, A38, A39, 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 A32, A36;
then A41: 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;
(E-max C) `1 = E-bound C by EUCLID:56;
then A42: ( (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 A41, A34, A35, GOBOARD7:8;

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, A2, A5, A30, A31, A42, A40, GOBOARD5:2;

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

A44: ( 1 <= j -' 1 & (j -' 1) + 1 <= width (Gauge C,n) ) by A1, A2, A21, A29, MATRIX_1:39, XREAL_1:237;
cell (Gauge C,n),((len (Gauge C,n)) -' 1),(j -' 1) meets C by A24, A13, A32, 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
A45: 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 A45;
A46: ( 1 <= (len (Gauge C,n)) -' 1 & ((len (Gauge C,n)) -' 1) + 1 <= len (Gauge C,n) ) by A37, NAT_D:49, XREAL_1:237;
A47: c in cell (Gauge C,n),((len (Gauge C,n)) -' 1),(j -' 1) by A45, XBOOLE_0:def 4;
then A48: ((Gauge C,n) * ((len (Gauge C,n)) -' 1),(j -' 1)) `1 <= c `1 by A46, A44, JORDAN9:19;
A49: c in C by A45, XBOOLE_0:def 4;
then c `1 <= E-bound C by PSCOMP_1:71;
then c in E-most C by A34, A49, A48, SPRECT_2:17, XXREAL_0:1;
then A50: c `2 <= (E-max C) `2 by PSCOMP_1:108;
((Gauge C,n) * ((len (Gauge C,n)) -' 1),(j -' 1)) `2 <= c `2 by A47, A46, A44, JORDAN9:19;
then ((Gauge C,n) * 1,(j -' 1)) `2 <= c `2 by A30, A31, A38, A39, GOBOARD5:2;
then ((Gauge C,n) * (len (Gauge C,n)),(j -' 1)) `2 <= c `2 by A5, A30, A31, GOBOARD5:2;
hence contradiction by A43, A50, XXREAL_0:2; :: thesis:

end;

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

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

end;

end;

end;

GoB (Cage C,n) = Gauge C,n by JORDAN1H:52;
then E-max C in right_cell (Cage C,n),((E-max (L~ (Cage C,n))) .. (Cage C,n)) by A24, A13, A33, JORDAN1H:29;
hence E-max C in right_cell (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))),1 by A6, Th7; :: thesis: