let n be 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 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:28;
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:42;
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:19, FINSEQ_4:20;
then A7: (Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = S-max (L~ (Cage (C,n))) by PARTFUN1:def 6;

A8: now :: thesis:

A9: 1 < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th3;
A10: 1 in dom (Cage (C,n)) by A5, FINSEQ_3:31;
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 6;
hence contradiction by A10, A9, FINSEQ_4:24; :: thesis:

end;

(S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= len (Cage (C,n)) by A5, FINSEQ_4:21;
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:235;
(Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (Gauge (C,n)) * (j,1) by A3, A6, PARTFUN1:def 6;
then A13: (Cage (C,n)) /. ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (GoB (Cage (C,n))) * (j,1) by JORDAN1H:44;
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:10;
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:25;
A19: ((S-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 in dom (Cage (C,n)) by A11, A17, FINSEQ_3:25;
then consider kj, ki being 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 9;
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:44;
A23: ki <= width (Gauge (C,n)) by A20, MATRIX_0:32;
A24: 1 <= kj by A20, MATRIX_0:32;
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_0:30;
then A26: [((j -' 1) + 1),1] in Indices (Gauge (C,n)) by A1, XREAL_1:235;
A27: 1 <= (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by Th3;
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:21;
then ((Gauge (C,n)) * (j,1)) `2 = ((Gauge (C,n)) * (kj,ki)) `2 by A3, A21, EUCLID:52;
then A29: ki = 1 by A20, A25, JORDAN1G:6;
[j,1] in Indices (GoB (Cage (C,n))) by A25, JORDAN1H:44;
then |.(1 - ki).| + |.(j - kj).| = 1 by A5, A18, A13, A22, FINSEQ_4:20, GOBOARD5:12;
then A30: 0 + |.(j - kj).| = 1 by A29, ABSVALUE:2;
A31: kj <= len (Gauge (C,n)) by A20, MATRIX_0:32;
2 <= len (Cage (C,n)) by GOBOARD7:34, 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:1, SPRECT_2:11;
then ((Gauge (C,n)) * (j,1)) `1 >= ((Gauge (C,n)) * (kj,ki)) `1 by A3, A21, PSCOMP_1:55;
then kj <= j by A1, A29, A23, A31, GOBOARD5:3;
then kj + 1 = j by A30, SEQM_3:41;
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_0:30;
(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:26;

A35: now :: thesis:

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:21;
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:235;
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:13;
( ((Gauge (C,n)) * (j,2)) `2 = S-bound C & (S-max C) `2 = S-bound C ) by A1, A2, EUCLID:52, JORDAN8:13;
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:8;

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

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:31;
then (cell ((Gauge (C,n)),(j -' 1),1)) /\ C <> {} by XBOOLE_0:def 7;
then consider c being object 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:24;
A50: ( (j -' 1) + 1 <= len (Gauge (C,n)) & 1 + 1 <= width (Gauge (C,n)) ) by A1, A2, A15, A41, XREAL_1:235, XXREAL_0:2;
then c `2 <= ((Gauge (C,n)) * ((j -' 1),(1 + 1))) `2 by A38, A47, JORDAN9:17;
then c in S-most C by A43, A48, A49, SPRECT_2:11, XXREAL_0:1;
then A51: c `1 <= (S-max C) `1 by PSCOMP_1:55;
((Gauge (C,n)) * ((j -' 1),1)) `1 <= c `1 by A38, A47, A50, JORDAN9:17;
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:53, SPRECT_1:12;
then consider r being object 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:84, PSCOMP_1:58;
then r in S-most (L~ (Cage (C,n))) by A54, SPRECT_2:11;
then (S-max (L~ (Cage (C,n)))) `1 >= r `1 by PSCOMP_1:55;
hence contradiction by A3, A52, A53, TOPREAL1:def 12; :: thesis:

end;

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