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

now

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

end;

then (S-max (L~ (Cage C,n))) .. (Cage C,n) < len (Cage C,n) by A7, XXREAL_0:1;
then A15: ((S-max (L~ (Cage C,n))) .. (Cage C,n)) + 1 <= len (Cage C,n) by NAT_1:13;
then A16: ((Cage C,n) /. (((S-max (L~ (Cage C,n))) .. (Cage C,n)) + 1)) `2 = S-bound (L~ (Cage C,n)) by A5, A10, JORDAN1E:25;
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 A15, FINSEQ_3:27;
then consider kj, ki being Element of NAT such that
A19: ( [kj,ki] in Indices (Gauge C,n) & (Cage C,n) /. (((S-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) = (Gauge C,n) * kj,ki ) by A2, GOBOARD1:def 11;
len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
then A20: [j,1] in Indices (Gauge C,n) by A1, A4, MATRIX_1:37;
((Gauge C,n) * j,1) `2 = ((Gauge C,n) * kj,ki) `2 by A1, A16, A19, EUCLID:56;
then A21: ki = 1 by A19, A20, JORDAN1G:6;
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 A16, A18, GOBOARD1:16, SPRECT_2:15;
then A22: ((Gauge C,n) * j,1) `1 >= ((Gauge C,n) * kj,ki) `1 by A1, A19, PSCOMP_1:118;
A23: ( 1 <= ki & ki <= width (Gauge C,n) & 1 <= j & 1 <= kj & kj <= len (Gauge C,n) ) by A1, A19, MATRIX_1:39;
then A24: kj <= j by A21, A22, GOBOARD5:4;
( (S-max (L~ (Cage C,n))) .. (Cage C,n) in dom (Cage C,n) & ((S-max (L~ (Cage C,n))) .. (Cage C,n)) + 1 in dom (Cage C,n) & [j,1] in Indices (GoB (Cage C,n)) & [kj,ki] in Indices (GoB (Cage C,n)) & (Cage C,n) /. ((S-max (L~ (Cage C,n))) .. (Cage C,n)) = (GoB (Cage C,n)) * j,1 & (Cage C,n) /. (((S-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) = (GoB (Cage C,n)) * kj,ki ) 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 0 + (abs (j - kj)) = 1 by A21, ABSVALUE:7;
then kj + 1 = j by A24, GOBOARD1:1;
then A25: kj = j - 1 ;
then A26: kj = j -' 1 by A23, NAT_D:39;
len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
then A27: [(j -' 1),1] in Indices (Gauge C,n) by A4, A23, A26, MATRIX_1:37;
( [((j -' 1) + 1),1] in Indices (Gauge C,n) & (Cage C,n) /. ((S-max (L~ (Cage C,n))) .. (Cage C,n)) = (Gauge C,n) * ((j -' 1) + 1),1 & (Cage C,n) /. (((S-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) = (Gauge C,n) * (j -' 1),1 ) by A1, A10, A19, A20, A21, A23, A25, NAT_D:39, XREAL_1:237;
then A28: 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 A2, A5, A15, A27, GOBRD13:27;
A29: GoB (Cage C,n) = Gauge C,n by JORDAN1H:52;

now

assume A30: not S-max C in right_cell (Cage C,n),((S-max (L~ (Cage C,n))) .. (Cage C,n)),(Gauge C,n) ; :: thesis:
1 < len (Gauge C,n) by A3, XXREAL_0:2;
then A31: 1 < width (Gauge C,n) by JORDAN8:def 1;
A32: ( 1 <= j -' 1 & j -' 1 <= len (Gauge C,n) ) by A23, A25, NAT_D:39;
then j -' 1 < j by NAT_D:51;
then j -' 1 < len (Gauge C,n) by A1, 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 A31, A32, 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 A33: not S-max C in LSeg ((Gauge C,n) * (j -' 1),2),((Gauge C,n) * j,2) by A28, A30;
A34: ((Gauge C,n) * (j -' 1),2) `2 = S-bound C by A32, JORDAN8:16;
A35: ((Gauge C,n) * j,2) `2 = S-bound C by A1, JORDAN8:16;
(S-max C) `2 = S-bound C by EUCLID:56;
then A36: ( (S-max C) `1 > ((Gauge C,n) * j,2) `1 or (S-max C) `1 < ((Gauge C,n) * (j -' 1),2) `1 ) by A33, A34, A35, GOBOARD7:9;
len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
then A37: 2 <= width (Gauge C,n) by A3, XXREAL_0:2;
A38: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;

per cases ) `1 < ((Gauge C,n) * (j -' 1),1) `1 or (S-max C) `1 > ((Gauge C,n) * j,1) `1 ) by A1, A32, A36, A37, GOBOARD5:3;

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

cell (Gauge C,n),(j -' 1),1 meets C by A5, A15, A28, JORDAN9:33;
then (cell (Gauge C,n),(j -' 1),1) /\ C <> {} by XBOOLE_0:def 7;
then consider c being set such that
A40: 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 A40;
A41: ( c in cell (Gauge C,n),(j -' 1),1 & c in C ) by A40, XBOOLE_0:def 4;
then A42: c `2 >= S-bound C by PSCOMP_1:71;
( (j -' 1) + 1 <= len (Gauge C,n) & 1 + 1 <= width (Gauge C,n) ) by A1, A3, A38, XREAL_1:237, XXREAL_0:2;
then A43: ( ((Gauge C,n) * (j -' 1),1) `1 <= c `1 & c `1 <= ((Gauge C,n) * ((j -' 1) + 1),1) `1 & ((Gauge C,n) * (j -' 1),1) `2 <= c `2 & c `2 <= ((Gauge C,n) * (j -' 1),(1 + 1)) `2 ) by A32, A41, JORDAN9:19;
then c in S-most C by A34, A41, A42, SPRECT_2:15, XXREAL_0:1;
then c `1 <= (S-max C) `1 by PSCOMP_1:118;
hence contradiction by A39, A43, XXREAL_0:2; :: thesis:

end;

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

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

end;

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