let i, n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for x, p being Point of (TOP-REAL 2) st x in E-most C & p in east_halfline x & 1 <= i & i < len (Cage C,n) & p in LSeg (Cage C,n),i holds
LSeg (Cage C,n),i is vertical
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for x, p being Point of (TOP-REAL 2) st x in E-most C & p in east_halfline x & 1 <= i & i < len (Cage C,n) & p in LSeg (Cage C,n),i holds
LSeg (Cage C,n),i is vertical
let x, p be Point of (TOP-REAL 2); :: thesis: ( x in E-most C & p in east_halfline x & 1 <= i & i < len (Cage C,n) & p in LSeg (Cage C,n),i implies LSeg (Cage C,n),i is vertical )
set G = Gauge C,n;
set f = Cage C,n;
assume that
A1: x in E-most C and
A2: p in east_halfline x and
A3: 1 <= i and
A4: i < len (Cage C,n) and
A5: p in LSeg (Cage C,n),i ; :: thesis: LSeg (Cage C,n),i is vertical
assume A6: not LSeg (Cage C,n),i is vertical ; :: thesis: contradiction
A7: i + 1 <= len (Cage C,n) by A4, NAT_1:13;
then A8: LSeg (Cage C,n),i = LSeg ((Cage C,n) /. i),((Cage C,n) /. (i + 1)) by A3, TOPREAL1:def 5;
1 <= i + 1 by A3, NAT_1:13;
then i + 1 in Seg (len (Cage C,n)) by A7, FINSEQ_1:3;
then A9: i + 1 in dom (Cage C,n) by FINSEQ_1:def 3;
i in Seg (len (Cage C,n)) by A3, A4, FINSEQ_1:3;
then A10: i in dom (Cage C,n) by FINSEQ_1:def 3;
p in L~ (Cage C,n) by A5, SPPOL_2:17;
then A11: p in (east_halfline x) /\ (L~ (Cage C,n)) by A2, XBOOLE_0:def 4;
A12: Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
A13: x `2 = p `2 by A2, TOPREAL1:def 13
.= ((Cage C,n) /. i) `2 by A5, A8, A6, SPPOL_1:41, SPPOL_1:63 ;
A14: x `2 = p `2 by A2, TOPREAL1:def 13
.= ((Cage C,n) /. (i + 1)) `2 by A5, A8, A6, SPPOL_1:41, SPPOL_1:63 ;
A15: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
then A16: (len (Gauge C,n)) -' 1 <= width (Gauge C,n) by NAT_D:35;
A17: x in C by A1, XBOOLE_0:def 4;

per cases ( ((Cage C,n) /. i) `1 <= ((Cage C,n) /. (i + 1)) `1 or ((Cage C,n) /. i) `1 >= ((Cage C,n) /. (i + 1)) `1 ) ;

suppose A18: ((Cage C,n) /. i) `1 <= ((Cage C,n) /. (i + 1)) `1 ; :: thesis: contradiction

then p `1 <= ((Cage C,n) /. (i + 1)) `1 by A5, A8, TOPREAL1:9;
then A19: ((Cage C,n) /. (i + 1)) `1 > x `1 by A17, A11, Th96, XXREAL_0:2;
consider i1, i2 being Element of NAT such that
A20: [i1,i2] in Indices (Gauge C,n) and
A21: (Cage C,n) /. (i + 1) = (Gauge C,n) * i1,i2 by A12, A9, GOBOARD1:def 11;
A22: ( 1 <= i2 & i2 <= width (Gauge C,n) ) by A20, MATRIX_1:39;
consider j1, j2 being Element of NAT such that
A23: [j1,j2] in Indices (Gauge C,n) and
A24: (Cage C,n) /. i = (Gauge C,n) * j1,j2 by A12, A10, GOBOARD1:def 11;
A25: ( 1 <= j2 & j2 <= width (Gauge C,n) ) by A23, MATRIX_1:39;
A26: i1 <= len (Gauge C,n) by A20, MATRIX_1:39;
A27: 1 <= i1 by A20, MATRIX_1:39;

now

assume ((Cage C,n) /. i) `1 = ((Cage C,n) /. (i + 1)) `1 ; :: thesis: contradiction
then A28: (Cage C,n) /. i = (Cage C,n) /. (i + 1) by A14, A13, TOPREAL3:11;
then A29: i2 = j2 by A20, A21, A23, A24, GOBOARD1:21;
( i1 = j1 & (abs (i1 - j1)) + (abs (i2 - j2)) = 1 ) by A12, A10, A9, A20, A21, A23, A24, A28, GOBOARD1:21, GOBOARD1:def 11;
then 1 = 0 + (abs (i2 - j2)) by GOBOARD7:2
.= 0 + 0 by A29, GOBOARD7:2 ;
hence contradiction ; :: thesis: verum

end;

then A30: ((Cage C,n) /. i) `1 < ((Cage C,n) /. (i + 1)) `1 by A18, XXREAL_0:1;
A31: 1 <= j1 by A23, MATRIX_1:39;
j1 <= len (Gauge C,n) by A23, MATRIX_1:39;
then i1 > j1 by A21, A22, A27, A24, A25, A30, Th39;
then len (Gauge C,n) > j1 by A26, XXREAL_0:2;
then A32: (len (Gauge C,n)) -' 1 >= j1 by NAT_D:49;
x `1 = (E-min C) `1 by A1, PSCOMP_1:108
.= E-bound C by EUCLID:56
.= ((Gauge C,n) * ((len (Gauge C,n)) -' 1),i2) `1 by A15, A22, JORDAN8:15 ;
then x `1 >= ((Cage C,n) /. i) `1 by A15, A16, A22, A24, A25, A31, A32, Th39;
then x in L~ (Cage C,n) by A8, A14, A13, A19, GOBOARD7:9, SPPOL_2:17;
then x in (L~ (Cage C,n)) /\ C by A17, XBOOLE_0:def 4;
then L~ (Cage C,n) meets C by XBOOLE_0:4;
hence contradiction by JORDAN10:5; :: thesis: verum

end;

suppose A33: ((Cage C,n) /. i) `1 >= ((Cage C,n) /. (i + 1)) `1 ; :: thesis: contradiction

then p `1 <= ((Cage C,n) /. i) `1 by A5, A8, TOPREAL1:9;
then A34: ((Cage C,n) /. i) `1 > x `1 by A17, A11, Th96, XXREAL_0:2;
consider i1, i2 being Element of NAT such that
A35: [i1,i2] in Indices (Gauge C,n) and
A36: (Cage C,n) /. i = (Gauge C,n) * i1,i2 by A12, A10, GOBOARD1:def 11;
A37: ( 1 <= i2 & i2 <= width (Gauge C,n) ) by A35, MATRIX_1:39;
consider j1, j2 being Element of NAT such that
A38: [j1,j2] in Indices (Gauge C,n) and
A39: (Cage C,n) /. (i + 1) = (Gauge C,n) * j1,j2 by A12, A9, GOBOARD1:def 11;
A40: ( 1 <= j2 & j2 <= width (Gauge C,n) ) by A38, MATRIX_1:39;
A41: i1 <= len (Gauge C,n) by A35, MATRIX_1:39;
A42: 1 <= i1 by A35, MATRIX_1:39;

now

assume ((Cage C,n) /. i) `1 = ((Cage C,n) /. (i + 1)) `1 ; :: thesis: contradiction
then A43: (Cage C,n) /. i = (Cage C,n) /. (i + 1) by A14, A13, TOPREAL3:11;
then A44: i2 = j2 by A35, A36, A38, A39, GOBOARD1:21;
( i1 = j1 & (abs (j1 - i1)) + (abs (j2 - i2)) = 1 ) by A12, A10, A9, A35, A36, A38, A39, A43, GOBOARD1:21, GOBOARD1:def 11;
then 1 = 0 + (abs (i2 - j2)) by A44, GOBOARD7:2
.= 0 + 0 by A44, GOBOARD7:2 ;
hence contradiction ; :: thesis: verum

end;

then A45: ((Cage C,n) /. (i + 1)) `1 < ((Cage C,n) /. i) `1 by A33, XXREAL_0:1;
A46: 1 <= j1 by A38, MATRIX_1:39;
j1 <= len (Gauge C,n) by A38, MATRIX_1:39;
then i1 > j1 by A36, A37, A42, A39, A40, A45, Th39;
then len (Gauge C,n) > j1 by A41, XXREAL_0:2;
then A47: (len (Gauge C,n)) -' 1 >= j1 by NAT_D:49;
x `1 = (E-min C) `1 by A1, PSCOMP_1:108
.= E-bound C by EUCLID:56
.= ((Gauge C,n) * ((len (Gauge C,n)) -' 1),i2) `1 by A15, A37, JORDAN8:15 ;
then x `1 >= ((Cage C,n) /. (i + 1)) `1 by A15, A16, A37, A39, A40, A46, A47, Th39;
then x in L~ (Cage C,n) by A8, A14, A13, A34, GOBOARD7:9, SPPOL_2:17;
then x in (L~ (Cage C,n)) /\ C by A17, XBOOLE_0:def 4;
then L~ (Cage C,n) meets C by XBOOLE_0:4;
hence contradiction by JORDAN10:5; :: thesis: verum

end;

end;