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 N-most C & p in north_halfline x & 1 <= i & i < len (Cage C,n) & p in LSeg (Cage C,n),i holds
LSeg (Cage C,n),i is horizontal
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 N-most C & p in north_halfline x & 1 <= i & i < len (Cage C,n) & p in LSeg (Cage C,n),i holds
LSeg (Cage C,n),i is horizontal
let x, p be Point of (TOP-REAL 2); :: thesis: ( x in N-most C & p in north_halfline x & 1 <= i & i < len (Cage C,n) & p in LSeg (Cage C,n),i implies LSeg (Cage C,n),i is horizontal )
set G = Gauge C,n;
set f = Cage C,n;
assume that
A1: x in N-most C and
A2: p in north_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 horizontal
A6: i + 1 <= len (Cage C,n) by A4, NAT_1:13;
then A7: LSeg (Cage C,n),i = LSeg ((Cage C,n) /. i),((Cage C,n) /. (i + 1)) by A3, TOPREAL1:def 5;
4 <= len (Gauge C,n) by JORDAN8:13;
then A8: 1 < len (Gauge C,n) by XXREAL_0:2;
A9: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
then A10: ( 1 <= (len (Gauge C,n)) -' 1 & (len (Gauge C,n)) -' 1 <= width (Gauge C,n) ) by A8, NAT_D:35, NAT_D:49;
assume A11: not LSeg (Cage C,n),i is horizontal ; :: thesis: contradiction
A12: x in C by A1, XBOOLE_0:def 4;
p in L~ (Cage C,n) by A5, SPPOL_2:17;
then A13: p in (north_halfline x) /\ (L~ (Cage C,n)) by A2, XBOOLE_0:def 4;
A14: x `1 = p `1 by A2, TOPREAL1:def 12
.= ((Cage C,n) /. (i + 1)) `1 by A5, A7, A11, SPPOL_1:41, SPPOL_1:64 ;
A15: x `1 = p `1 by A2, TOPREAL1:def 12
.= ((Cage C,n) /. i) `1 by A5, A7, A11, SPPOL_1:41, SPPOL_1:64 ;
A16: Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
i in Seg (len (Cage C,n)) by A3, A4, FINSEQ_1:3;
then A17: i in dom (Cage C,n) by FINSEQ_1:def 3;
1 <= i + 1 by A3, NAT_1:13;
then i + 1 in Seg (len (Cage C,n)) by A6, FINSEQ_1:3;
then A18: i + 1 in dom (Cage C,n) by FINSEQ_1:def 3;

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

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

then p `2 <= ((Cage C,n) /. (i + 1)) `2 by A5, A7, TOPREAL1:10;
then A20: ((Cage C,n) /. (i + 1)) `2 > x `2 by A12, A13, Th95, XXREAL_0:2;
consider i1, i2 being Element of NAT such that
A21: [i1,i2] in Indices (Gauge C,n) and
A22: (Cage C,n) /. (i + 1) = (Gauge C,n) * i1,i2 by A16, A18, GOBOARD1:def 11;
A23: ( 1 <= i2 & i2 <= width (Gauge C,n) & 1 <= i1 & i1 <= len (Gauge C,n) ) by A21, MATRIX_1:39;
then A24: ( 1 <= i2 & i2 <= len (Gauge C,n) ) by JORDAN8:def 1;
A25: x `2 = (N-min C) `2 by A1, PSCOMP_1:98
.= N-bound C by EUCLID:56
.= ((Gauge C,n) * i1,((len (Gauge C,n)) -' 1)) `2 by A23, JORDAN8:17 ;
consider j1, j2 being Element of NAT such that
A26: [j1,j2] in Indices (Gauge C,n) and
A27: (Cage C,n) /. i = (Gauge C,n) * j1,j2 by A16, A17, GOBOARD1:def 11;
A28: ( 1 <= j2 & j2 <= width (Gauge C,n) & 1 <= j1 & j1 <= len (Gauge C,n) ) by A26, MATRIX_1:39;

now

assume ((Cage C,n) /. i) `2 = ((Cage C,n) /. (i + 1)) `2 ; :: thesis: contradiction
then A29: (Cage C,n) /. i = (Cage C,n) /. (i + 1) by A14, A15, TOPREAL3:11;
then A30: ( i1 = j1 & i2 = j2 ) by A21, A22, A26, A27, GOBOARD1:21;
(abs (i1 - j1)) + (abs (i2 - j2)) = 1 by A16, A17, A18, A21, A22, A26, A27, A29, GOBOARD1:def 11;
then 1 = 0 + (abs (i2 - j2)) by A30, GOBOARD7:2
.= 0 + 0 by A30, GOBOARD7:2 ;
hence contradiction ; :: thesis: verum

end;

then ((Cage C,n) /. i) `2 < ((Cage C,n) /. (i + 1)) `2 by A19, XXREAL_0:1;
then i2 > j2 by A22, A23, A27, A28, Th40;
then len (Gauge C,n) > j2 by A24, XXREAL_0:2;
then (len (Gauge C,n)) -' 1 >= j2 by NAT_D:49;
then x `2 >= ((Cage C,n) /. i) `2 by A10, A23, A25, A27, A28, Th40;
then x in L~ (Cage C,n) by A7, A14, A15, A20, GOBOARD7:8, SPPOL_2:17;
then L~ (Cage C,n) meets C by A12, XBOOLE_0:3;
hence contradiction by JORDAN10:5; :: thesis: verum

end;

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

then p `2 <= ((Cage C,n) /. i) `2 by A5, A7, TOPREAL1:10;
then A32: ((Cage C,n) /. i) `2 > x `2 by A12, A13, Th95, XXREAL_0:2;
consider i1, i2 being Element of NAT such that
A33: [i1,i2] in Indices (Gauge C,n) and
A34: (Cage C,n) /. i = (Gauge C,n) * i1,i2 by A16, A17, GOBOARD1:def 11;
A35: ( 1 <= i2 & i2 <= width (Gauge C,n) & 1 <= i1 & i1 <= len (Gauge C,n) ) by A33, MATRIX_1:39;
A36: x `2 = (N-min C) `2 by A1, PSCOMP_1:98
.= N-bound C by EUCLID:56
.= ((Gauge C,n) * i1,((len (Gauge C,n)) -' 1)) `2 by A35, JORDAN8:17 ;
consider j1, j2 being Element of NAT such that
A37: [j1,j2] in Indices (Gauge C,n) and
A38: (Cage C,n) /. (i + 1) = (Gauge C,n) * j1,j2 by A16, A18, GOBOARD1:def 11;
A39: ( 1 <= j2 & j2 <= width (Gauge C,n) & 1 <= j1 & j1 <= len (Gauge C,n) ) by A37, MATRIX_1:39;

now

assume ((Cage C,n) /. i) `2 = ((Cage C,n) /. (i + 1)) `2 ; :: thesis: contradiction
then A40: (Cage C,n) /. i = (Cage C,n) /. (i + 1) by A14, A15, TOPREAL3:11;
then A41: ( i1 = j1 & i2 = j2 ) by A33, A34, A37, A38, GOBOARD1:21;
(abs (j1 - i1)) + (abs (j2 - i2)) = 1 by A16, A17, A18, A33, A34, A37, A38, A40, GOBOARD1:def 11;
then 1 = 0 + (abs (i2 - j2)) by A41, GOBOARD7:2
.= 0 + 0 by A41, GOBOARD7:2 ;
hence contradiction ; :: thesis: verum

end;

then ((Cage C,n) /. (i + 1)) `2 < ((Cage C,n) /. i) `2 by A31, XXREAL_0:1;
then i2 > j2 by A34, A35, A38, A39, Th40;
then len (Gauge C,n) > j2 by A9, A35, XXREAL_0:2;
then (len (Gauge C,n)) -' 1 >= j2 by NAT_D:49;
then x `2 >= ((Cage C,n) /. (i + 1)) `2 by A10, A35, A36, A38, A39, Th40;
then x in L~ (Cage C,n) by A7, A14, A15, A32, GOBOARD7:8, SPPOL_2:17;
then x in (L~ (Cage C,n)) /\ C by A12, XBOOLE_0:def 4;
then L~ (Cage C,n) meets C by XBOOLE_0:4;
hence contradiction by JORDAN10:5; :: thesis: verum

end;

end;