let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i < len (Cage C,n) & N-max C in right_cell (Cage C,n),i,(Gauge C,n) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ex i being Element of NAT st
( 1 <= i & i < len (Cage C,n) & N-max C in right_cell (Cage C,n),i,(Gauge C,n) )
consider p being Point of (TOP-REAL 2) such that
A1: (north_halfline (N-max C)) /\ (L~ (Cage C,n)) = {p} by JORDAN1A:107, PSCOMP_1:101;
A2: p in (north_halfline (N-max C)) /\ (L~ (Cage C,n)) by A1, TARSKI:def 1;
then A3: p in north_halfline (N-max C) by XBOOLE_0:def 4;
p in L~ (Cage C,n) by A2, XBOOLE_0:def 4;
then consider i being Element of NAT such that
A4: 1 <= i and
A5: i + 1 <= len (Cage C,n) and
A6: p in LSeg (Cage C,n),i by SPPOL_2:13;
take i ; :: thesis: ( 1 <= i & i < len (Cage C,n) & N-max C in right_cell (Cage C,n),i,(Gauge C,n) )
A7: LSeg (Cage C,n),i = LSeg ((Cage C,n) /. i),((Cage C,n) /. (i + 1)) by A4, A5, TOPREAL1:def 5;
A8: len (Gauge C,n) >= 4 by JORDAN8:13;
then A9: 1 < len (Gauge C,n) by XXREAL_0:2;
A10: ((len (Gauge C,n)) -' 1) + 1 = len (Gauge C,n) by A8, XREAL_1:237, XXREAL_0:2;
then A11: (len (Gauge C,n)) -' 1 < len (Gauge C,n) by NAT_1:13;
A12: N-max C = |[((N-max C) `1 ),((N-max C) `2 )]| by EUCLID:57;
A13: (len (Gauge C,n)) -' 1 <= len (Gauge C,n) by NAT_D:44;
A14: (N-max C) `2 = N-bound C by EUCLID:56
.= ((Gauge C,n) * 1,((len (Gauge C,n)) -' 1)) `2 by A9, JORDAN8:17 ;
A15: N-max C in N-most C by PSCOMP_1:101;
A16: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
thus A17: ( 1 <= i & i < len (Cage C,n) ) by A4, A5, NAT_1:13; :: thesis: N-max C in right_cell (Cage C,n),i,(Gauge C,n)
then A18: ((Cage C,n) /. i) `2 = p `2 by A3, A6, A15, A7, JORDAN1A:99, SPPOL_1:63;
A19: ((Cage C,n) /. (i + 1)) `2 = p `2 by A3, A6, A17, A15, A7, JORDAN1A:99, SPPOL_1:63;
A20: 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
A21: [i1,j1] in Indices (Gauge C,n) and
A22: (Cage C,n) /. i = (Gauge C,n) * i1,j1 and
A23: [i2,j2] in Indices (Gauge C,n) and
A24: (Cage C,n) /. (i + 1) = (Gauge C,n) * i2,j2 and
A25: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A4, A5, JORDAN8:6;
A26: 1 <= i1 by A21, MATRIX_1:39;
A27: j2 <= width (Gauge C,n) by A23, MATRIX_1:39;
A28: i1 <= len (Gauge C,n) by A21, MATRIX_1:39;
A29: 1 <= j1 by A21, MATRIX_1:39;
p `2 = N-bound (L~ (Cage C,n)) by A2, JORDAN1A:103, PSCOMP_1:101;
then ((Gauge C,n) * i1,j1) `2 = ((Gauge C,n) * i1,(len (Gauge C,n))) `2 by A22, A18, A26, A28, JORDAN1A:91;
then A30: len (Gauge C,n) <= j1 by A16, A26, A28, A29, GOBOARD5:5;
A31: j1 <= width (Gauge C,n) by A21, MATRIX_1:39;
then A32: j1 = len (Gauge C,n) by A16, A30, XXREAL_0:1;
A33: 1 <= j2 by A23, MATRIX_1:39;
A34: j1 = j2

proof

assume j1 <> j2 ; :: thesis: contradiction
then ( j1 < j2 or j2 < j1 ) by XXREAL_0:1;
hence contradiction by A22, A24, A25, A18, A19, A26, A28, A29, A27, A33, A31, GOBOARD5:5; :: thesis: verum

end;

A35: 1 <= i2 by A23, MATRIX_1:39;
A36: i2 <= len (Gauge C,n) by A23, MATRIX_1:39;
i1 <= i1 + 1 by NAT_1:11;
then A37: ((Cage C,n) /. i) `1 <= ((Cage C,n) /. (i + 1)) `1 by A4, A5, A21, A22, A23, A24, A25, A16, A26, A36, A29, A27, A34, A30, JORDAN10:4, JORDAN1A:39;
then p `1 <= ((Cage C,n) /. (i + 1)) `1 by A6, A7, TOPREAL1:9;
then (N-max C) `1 <= ((Gauge C,n) * (i1 + 1),(len (Gauge C,n))) `1 by A3, A4, A5, A21, A22, A23, A24, A25, A16, A34, A32, JORDAN10:4, TOPREAL1:def 12;
then A38: (N-max C) `1 <= ((Gauge C,n) * (i1 + 1),1) `1 by A4, A5, A21, A22, A23, A24, A25, A16, A35, A36, A34, A30, A9, GOBOARD5:3, JORDAN10:4;
((Cage C,n) /. i) `1 <= p `1 by A6, A7, A37, TOPREAL1:9;
then ((Gauge C,n) * i1,(len (Gauge C,n))) `1 <= (N-max C) `1 by A3, A22, A32, TOPREAL1:def 12;
then A39: ((Gauge C,n) * i1,1) `1 <= (N-max C) `1 by A16, A26, A28, A9, GOBOARD5:3;
len (Gauge C,n) >= 1 + 1 by A8, XXREAL_0:2;
then A40: (len (Gauge C,n)) - 1 >= 1 by XREAL_1:21;
then (len (Gauge C,n)) -' 1 >= 1 by XREAL_0:def 2;
then ((Gauge C,n) * 1,j1) `2 >= (N-max C) `2 by A16, A32, A9, A14, A13, SPRECT_3:24;
then A41: N-max C in { |[r,s]| where r, s is Real : ( ((Gauge C,n) * i1,1) `1 <= r & r <= ((Gauge C,n) * (i1 + 1),1) `1 & ((Gauge C,n) * 1,(j1 -' 1)) `2 <= s & s <= ((Gauge C,n) * 1,j1) `2 ) } by A32, A14, A39, A38, A12;
A42: 1 <= i1 by A21, MATRIX_1:39;
i1 < len (Gauge C,n) by A4, A5, A21, A22, A23, A24, A25, A16, A36, A34, A30, JORDAN10:4, NAT_1:13;
then N-max C in cell (Gauge C,n),i1,(j1 -' 1) by A16, A32, A42, A40, A10, A11, A41, GOBRD11:32;
hence N-max C in right_cell (Cage C,n),i,(Gauge C,n) by A4, A5, A20, A21, A22, A23, A24, A25, A16, A34, A30, GOBRD13:25, JORDAN10:4; :: thesis: verum