let n be Element of NAT ; :: thesis:
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
consider p being Point of (TOP-REAL 2) such that
A1: (south_halfline (S-min C)) /\ (L~ (Cage C,n)) = {p} by JORDAN1A:109, PSCOMP_1:121;
A2: p in (south_halfline (S-min C)) /\ (L~ (Cage C,n)) by A1, TARSKI:def 1;
then A3: p in south_halfline (S-min C) by XBOOLE_0:def 4;
A4: S-min C = |[((S-min C) `1 ),((S-min C) `2 )]| by EUCLID:57;
A5: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
A6: len (Gauge C,n) >= 4 by JORDAN8:13;
then A7: 1 < len (Gauge C,n) by XXREAL_0:2;
p in L~ (Cage C,n) by A2, XBOOLE_0:def 4;
then consider i being Element of NAT such that
A8: 1 <= i and
A9: i + 1 <= len (Cage C,n) and
A10: p in LSeg (Cage C,n),i by SPPOL_2:13;
take i ; :: thesis:
A11: LSeg (Cage C,n),i = LSeg ((Cage C,n) /. i),((Cage C,n) /. (i + 1)) by A8, A9, TOPREAL1:def 5;
A12: (S-min C) `2 = S-bound C by EUCLID:56
.= ((Gauge C,n) * 1,2) `2 by A7, JORDAN8:16 ;
A13: S-min C in S-most C by PSCOMP_1:121;
thus A14: ( 1 <= i & i < len (Cage C,n) ) by A8, A9, NAT_1:13; :: thesis:
then A15: ((Cage C,n) /. i) `2 = p `2 by A3, A10, A13, A11, JORDAN1A:101, SPPOL_1:63;
A16: Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
then consider i1, j1, i2, j2 being Element of NAT such that
A17: [i1,j1] in Indices (Gauge C,n) and
A18: (Cage C,n) /. i = (Gauge C,n) * i1,j1 and
A19: [i2,j2] in Indices (Gauge C,n) and
A20: (Cage C,n) /. (i + 1) = (Gauge C,n) * i2,j2 and
A21: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A8, A9, JORDAN8:6;
A22: 1 <= i1 by A17, MATRIX_1:39;
A23: 1 <= j2 by A19, MATRIX_1:39;
A24: i2 <= i2 + 1 by NAT_1:11;
A25: j2 <= width (Gauge C,n) by A19, MATRIX_1:39;
A26: i1 <= len (Gauge C,n) by A17, MATRIX_1:39;
A27: j1 <= width (Gauge C,n) by A17, MATRIX_1:39;
p `2 = S-bound (L~ (Cage C,n)) by A2, JORDAN1A:105, PSCOMP_1:121;
then ((Gauge C,n) * i1,j1) `2 = ((Gauge C,n) * i1,1) `2 by A18, A15, A22, A26, JORDAN1A:93;
then A28: 1 >= j1 by A22, A26, A27, GOBOARD5:5;
A29: 1 <= j1 by A17, MATRIX_1:39;
then A30: j1 = 1 by A28, XXREAL_0:1;
A31: ((Cage C,n) /. (i + 1)) `2 = p `2 by A3, A10, A14, A13, A11, JORDAN1A:101, SPPOL_1:63;
A32: j1 = j2

proof

assume j1 <> j2 ; :: thesis:
then ( j1 < j2 or j2 < j1 ) by XXREAL_0:1;
hence contradiction by A18, A20, A21, A15, A31, A22, A26, A29, A25, A23, A27, GOBOARD5:5; :: thesis:

end;

then A33: i2 < len (Gauge C,n) by A8, A9, A17, A18, A19, A20, A21, A26, A28, JORDAN10:3, NAT_1:13;
1 <= i2 by A19, MATRIX_1:39;
then A34: ((Cage C,n) /. i) `1 >= ((Cage C,n) /. (i + 1)) `1 by A8, A9, A17, A18, A19, A20, A21, A26, A29, A25, A23, A27, A28, A24, JORDAN10:3, JORDAN1A:39;
then p `1 <= ((Cage C,n) /. i) `1 by A10, A11, TOPREAL1:9;
then A35: (S-min C) `1 <= ((Gauge C,n) * (i2 + 1),1) `1 by A3, A8, A9, A17, A18, A19, A20, A21, A32, A30, JORDAN10:3, TOPREAL1:def 14;
((Cage C,n) /. (i + 1)) `1 <= p `1 by A10, A11, A34, TOPREAL1:9;
then A36: ((Gauge C,n) * i2,1) `1 <= (S-min C) `1 by A3, A20, A32, A30, TOPREAL1:def 14;
A37: 1 <= i2 by A19, MATRIX_1:39;
1 + 1 <= len (Gauge C,n) by A6, XXREAL_0:2;
then ((Gauge C,n) * 1,j1) `2 <= (S-min C) `2 by A5, A30, A7, A12, SPRECT_3:24;
then S-min C in { |[r,s]| where r, s is Real : ( ((Gauge C,n) * i2,1) `1 <= r & r <= ((Gauge C,n) * (i2 + 1),1) `1 & ((Gauge C,n) * 1,j1) `2 <= s & s <= ((Gauge C,n) * 1,(j1 + 1)) `2 ) } by A30, A12, A36, A35, A4;
then S-min C in cell (Gauge C,n),i2,j1 by A5, A30, A37, A33, A7, GOBRD11:32;
hence S-min C in right_cell (Cage C,n),i,(Gauge C,n) by A8, A9, A16, A17, A18, A19, A20, A21, A32, A28, GOBRD13:27, JORDAN10:3; :: thesis: