let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i < len (Cage (C,n)) & E-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 Nat st
( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
consider p being Point of (TOP-REAL 2) such that
A1: (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) = {p} by JORDAN1A:87, PSCOMP_1:50;
A2: p in (east_halfline (E-max C)) /\ (L~ (Cage (C,n))) by A1, TARSKI:def 1;
then A3: p in east_halfline (E-max C) by XBOOLE_0:def 4;
len (Gauge (C,n)) < (len (Gauge (C,n))) + 1 by NAT_1:13;
then A4: (len (Gauge (C,n))) - 1 < len (Gauge (C,n)) by XREAL_1:19;
A5: (len (Gauge (C,n))) -' 1 <= len (Gauge (C,n)) by NAT_D:44;
A6: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A7: 1 < len (Gauge (C,n)) by XXREAL_0:2;
A8: ((len (Gauge (C,n))) -' 1) + 1 = len (Gauge (C,n)) by A6, XREAL_1:235, XXREAL_0:2;
A9: (E-max C) `1 = E-bound C by EUCLID:52
.= ((Gauge (C,n)) * (((len (Gauge (C,n))) -' 1),1)) `1 by A7, JORDAN8:12 ;
A10: E-max C = |[((E-max C) `1),((E-max C) `2)]| by EUCLID:53;
A11: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
A12: E-max C in E-most C by PSCOMP_1:50;
p in L~ (Cage (C,n)) by A2, XBOOLE_0:def 4;
then consider i being Nat such that
A13: 1 <= i and
A14: i + 1 <= len (Cage (C,n)) and
A15: p in LSeg ((Cage (C,n)),i) by SPPOL_2:13;
take i ; :: thesis: ( 1 <= i & i < len (Cage (C,n)) & E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n))) )
A16: LSeg ((Cage (C,n)),i) = LSeg (((Cage (C,n)) /. i),((Cage (C,n)) /. (i + 1))) by A13, A14, TOPREAL1:def 3;
thus A17: ( 1 <= i & i < len (Cage (C,n)) ) by A13, A14, NAT_1:13; :: thesis: E-max C in right_cell ((Cage (C,n)),i,(Gauge (C,n)))
then A18: ((Cage (C,n)) /. i) `1 = p `1 by A3, A15, A12, A16, JORDAN1A:79, SPPOL_1:41;
A19: ((Cage (C,n)) /. (i + 1)) `1 = p `1 by A3, A15, A17, A12, A16, JORDAN1A:79, SPPOL_1:41;
A20: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
then consider i1, j1, i2, j2 being 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 A13, A14, JORDAN8:3;
A26: 1 <= i1 by A21, MATRIX_0:32;
A27: j1 <= width (Gauge (C,n)) by A21, MATRIX_0:32;
A28: i2 <= len (Gauge (C,n)) by A23, MATRIX_0:32;
A29: j2 <= width (Gauge (C,n)) by A23, MATRIX_0:32;
A30: 1 <= j1 by A21, MATRIX_0:32;
p `1 = E-bound (L~ (Cage (C,n))) by A2, JORDAN1A:83, PSCOMP_1:50;
then ((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * ((len (Gauge (C,n))),j1)) `1 by A22, A18, A11, A30, A27, JORDAN1A:71;
then A31: len (Gauge (C,n)) <= i1 by A26, A30, A27, GOBOARD5:3;
A32: i1 <= len (Gauge (C,n)) by A21, MATRIX_0:32;
then A33: i1 = len (Gauge (C,n)) by A31, XXREAL_0:1;
A34: 1 <= i2 by A23, MATRIX_0:32;
A35: i1 = i2

proof

assume i1 <> i2 ; :: thesis: contradiction
then ( i1 < i2 or i2 < i1 ) by XXREAL_0:1;
hence contradiction by A22, A24, A25, A18, A19, A26, A32, A34, A28, A30, A29, GOBOARD5:3; :: thesis: verum

end;

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