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 <= len (Gauge C,n) and
A3: S-max (L~ (Cage C,n)) = (Gauge C,n) * j,1 by JORDAN1D:32;
A4: Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
set k = (S-max (L~ (Cage C,n))) .. (Cage C,n);
A5: S-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:46;
then A6: ( (S-max (L~ (Cage C,n))) .. (Cage C,n) in dom (Cage C,n) & (Cage C,n) . ((S-max (L~ (Cage C,n))) .. (Cage C,n)) = S-max (L~ (Cage C,n)) ) by FINSEQ_4:29, FINSEQ_4:30;
then A7: (Cage C,n) /. ((S-max (L~ (Cage C,n))) .. (Cage C,n)) = S-max (L~ (Cage C,n)) by PARTFUN1:def 8;

A8: now

A9: 1 < (S-max (L~ (Cage C,n))) .. (Cage C,n) by Th5;
A10: 1 in dom (Cage C,n) by A5, FINSEQ_3:33;
assume (S-max (L~ (Cage C,n))) .. (Cage C,n) = len (Cage C,n) ; :: thesis:
then (Cage C,n) /. 1 = S-max (L~ (Cage C,n)) by A7, FINSEQ_6:def 1;
then (Cage C,n) . 1 = S-max (L~ (Cage C,n)) by A10, PARTFUN1:def 8;
hence contradiction by A10, A9, FINSEQ_4:34; :: thesis:

end;

(S-max (L~ (Cage C,n))) .. (Cage C,n) <= len (Cage C,n) by A5, FINSEQ_4:31;
then (S-max (L~ (Cage C,n))) .. (Cage C,n) < len (Cage C,n) by A8, XXREAL_0:1;
then A11: ((S-max (L~ (Cage C,n))) .. (Cage C,n)) + 1 <= len (Cage C,n) by NAT_1:13;
A12: (Cage C,n) /. ((S-max (L~ (Cage C,n))) .. (Cage C,n)) = (Gauge C,n) * ((j -' 1) + 1),1 by A1, A3, A7, XREAL_1:237;
(Cage C,n) /. ((S-max (L~ (Cage C,n))) .. (Cage C,n)) = (Gauge C,n) * j,1 by A3, A6, PARTFUN1:def 8;
then A13: (Cage C,n) /. ((S-max (L~ (Cage C,n))) .. (Cage C,n)) = (GoB (Cage C,n)) * j,1 by JORDAN1H:52;
set p = S-max C;
A14: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
A15: len (Gauge C,n) >= 4 by JORDAN8:13;
then A16: 1 <= len (Gauge C,n) by XXREAL_0:2;
A17: 1 <= ((S-max (L~ (Cage C,n))) .. (Cage C,n)) + 1 by NAT_1:11;
then A18: ((S-max (L~ (Cage C,n))) .. (Cage C,n)) + 1 in dom (Cage C,n) by A11, FINSEQ_3:27;
A19: ((S-max (L~ (Cage C,n))) .. (Cage C,n)) + 1 in dom (Cage C,n) by A11, A17, FINSEQ_3:27;
then consider kj, ki being Element of NAT such that
A20: [kj,ki] in Indices (Gauge C,n) and
A21: (Cage C,n) /. (((S-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) = (Gauge C,n) * kj,ki by A4, GOBOARD1:def 11;
A22: ( [kj,ki] in Indices (GoB (Cage C,n)) & (Cage C,n) /. (((S-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) = (GoB (Cage C,n)) * kj,ki ) by A20, A21, JORDAN1H:52;
A23: ki <= width (Gauge C,n) by A20, MATRIX_1:39;
A24: 1 <= kj by A20, MATRIX_1:39;
len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
then A25: [j,1] in Indices (Gauge C,n) by A1, A2, A16, MATRIX_1:37;
then A26: [((j -' 1) + 1),1] in Indices (Gauge C,n) by A1, XREAL_1:237;
A27: 1 <= (S-max (L~ (Cage C,n))) .. (Cage C,n) by Th5;
then A28: ((Cage C,n) /. (((S-max (L~ (Cage C,n))) .. (Cage C,n)) + 1)) `2 = S-bound (L~ (Cage C,n)) by A7, A11, JORDAN1E:25;
then ((Gauge C,n) * j,1) `2 = ((Gauge C,n) * kj,ki) `2 by A3, A21, EUCLID:56;
then A29: ki = 1 by A20, A25, JORDAN1G:6;
[j,1] in Indices (GoB (Cage C,n)) by A25, JORDAN1H:52;
then (abs (1 - ki)) + (abs (j - kj)) = 1 by A5, A18, A13, A22, FINSEQ_4:30, GOBOARD5:13;
then A30: 0 + (abs (j - kj)) = 1 by A29, ABSVALUE:7;
A31: kj <= len (Gauge C,n) by A20, MATRIX_1:39;
2 <= len (Cage C,n) by GOBOARD7:36, XXREAL_0:2;
then (Cage C,n) /. (((S-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) in S-most (L~ (Cage C,n)) by A28, A19, GOBOARD1:16, SPRECT_2:15;
then ((Gauge C,n) * j,1) `1 >= ((Gauge C,n) * kj,ki) `1 by A3, A21, PSCOMP_1:118;
then kj <= j by A1, A29, A23, A31, GOBOARD5:4;
then kj + 1 = j by A30, SEQM_3:81;
then A32: kj = j - 1 ;
then kj = j -' 1 by A24, NAT_D:39;
then A33: [(j -' 1),1] in Indices (Gauge C,n) by A16, A24, A31, A14, MATRIX_1:37;
(Cage C,n) /. (((S-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) = (Gauge C,n) * (j -' 1),1 by A21, A29, A24, A32, NAT_D:39;
then A34: right_cell (Cage C,n),((S-max (L~ (Cage C,n))) .. (Cage C,n)),(Gauge C,n) = cell (Gauge C,n),(j -' 1),1 by A4, A27, A11, A33, A26, A12, GOBRD13:27;

A35: now

1 < len (Gauge C,n) by A15, XXREAL_0:2;
then A36: 1 < width (Gauge C,n) by JORDAN8:def 1;
assume A37: not S-max C in right_cell (Cage C,n),((S-max (L~ (Cage C,n))) .. (Cage C,n)),(Gauge C,n) ; :: thesis:
A38: 1 <= j -' 1 by A24, A32, NAT_D:39;
then j -' 1 < j by NAT_D:51;
then j -' 1 < len (Gauge C,n) by A2, XXREAL_0:2;
then LSeg ((Gauge C,n) * (j -' 1),(1 + 1)),((Gauge C,n) * ((j -' 1) + 1),(1 + 1)) c= cell (Gauge C,n),(j -' 1),1 by A36, A38, GOBOARD5:22;
then LSeg ((Gauge C,n) * (j -' 1),2),((Gauge C,n) * j,2) c= cell (Gauge C,n),(j -' 1),1 by A1, XREAL_1:237;
then A39: not S-max C in LSeg ((Gauge C,n) * (j -' 1),2),((Gauge C,n) * j,2) by A34, A37;
len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
then A40: 2 <= width (Gauge C,n) by A15, XXREAL_0:2;
A41: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
A42: j -' 1 <= len (Gauge C,n) by A24, A31, A32, NAT_D:39;
then A43: ((Gauge C,n) * (j -' 1),2) `2 = S-bound C by A38, JORDAN8:16;
( ((Gauge C,n) * j,2) `2 = S-bound C & (S-max C) `2 = S-bound C ) by A1, A2, EUCLID:56, JORDAN8:16;
then A44: ( (S-max C) `1 > ((Gauge C,n) * j,2) `1 or (S-max C) `1 < ((Gauge C,n) * (j -' 1),2) `1 ) by A39, A43, GOBOARD7:9;

per cases ) `1 < ((Gauge C,n) * (j -' 1),1) `1 or (S-max C) `1 > ((Gauge C,n) * j,1) `1 ) by A1, A2, A38, A42, A44, A40, GOBOARD5:3;

suppose A45: (S-max C) `1 < ((Gauge C,n) * (j -' 1),1) `1 ; :: thesis:

cell (Gauge C,n),(j -' 1),1 meets C by A27, A11, A34, JORDAN9:33;
then (cell (Gauge C,n),(j -' 1),1) /\ C <> {} by XBOOLE_0:def 7;
then consider c being set such that
A46: c in (cell (Gauge C,n),(j -' 1),1) /\ C by XBOOLE_0:def 1;
reconsider c = c as Element of (TOP-REAL 2) by A46;
A47: c in cell (Gauge C,n),(j -' 1),1 by A46, XBOOLE_0:def 4;
A48: c in C by A46, XBOOLE_0:def 4;
then A49: c `2 >= S-bound C by PSCOMP_1:71;
A50: ( (j -' 1) + 1 <= len (Gauge C,n) & 1 + 1 <= width (Gauge C,n) ) by A1, A2, A15, A41, XREAL_1:237, XXREAL_0:2;
then c `2 <= ((Gauge C,n) * (j -' 1),(1 + 1)) `2 by A38, A47, JORDAN9:19;
then c in S-most C by A43, A48, A49, SPRECT_2:15, XXREAL_0:1;
then A51: c `1 <= (S-max C) `1 by PSCOMP_1:118;
((Gauge C,n) * (j -' 1),1) `1 <= c `1 by A38, A47, A50, JORDAN9:19;
hence contradiction by A45, A51, XXREAL_0:2; :: thesis:

end;

suppose A52: (S-max C) `1 > ((Gauge C,n) * j,1) `1 ; :: thesis:

south_halfline (S-max C) meets L~ (Cage C,n) by JORDAN1A:74, SPRECT_1:14;
then consider r being set such that
A53: r in south_halfline (S-max C) and
A54: r in L~ (Cage C,n) by XBOOLE_0:3;
reconsider r = r as Element of (TOP-REAL 2) by A53;
r in (south_halfline (S-max C)) /\ (L~ (Cage C,n)) by A53, A54, XBOOLE_0:def 4;
then r `2 = S-bound (L~ (Cage C,n)) by JORDAN1A:105, PSCOMP_1:121;
then r in S-most (L~ (Cage C,n)) by A54, SPRECT_2:15;
then (S-max (L~ (Cage C,n))) `1 >= r `1 by PSCOMP_1:118;
hence contradiction by A3, A52, A53, TOPREAL1:def 14; :: thesis:

end;

end;

end;

GoB (Cage C,n) = Gauge C,n by JORDAN1H:52;
then S-max C in right_cell (Cage C,n),((S-max (L~ (Cage C,n))) .. (Cage C,n)) by A27, A11, A35, JORDAN1H:29;
hence S-max C in right_cell (Rotate (Cage C,n),(S-max (L~ (Cage C,n)))),1 by A5, Th7; :: thesis: