let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being Element of NAT st 1 < i & i <= len (Gauge C,n) holds
not (Gauge C,n) * i,1 in L~ (Upper_Seq C,n)
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for i being Element of NAT st 1 < i & i <= len (Gauge C,n) holds
not (Gauge C,n) * i,1 in L~ (Upper_Seq C,n)
let i be Element of NAT ; :: thesis: ( 1 < i & i <= len (Gauge C,n) implies not (Gauge C,n) * i,1 in L~ (Upper_Seq C,n) )
assume that
A1: ( 1 < i & i <= len (Gauge C,n) ) and
A2: (Gauge C,n) * i,1 in L~ (Upper_Seq C,n) ; :: thesis: contradiction
set Gi1 = (Gauge C,n) * i,1;
consider ii being Element of NAT such that
A3: 1 <= ii and
A4: ii + 1 <= len (Upper_Seq C,n) and
A5: (Gauge C,n) * i,1 in LSeg (Upper_Seq C,n),ii by A2, SPPOL_2:13;
A6: LSeg (Upper_Seq C,n),ii = LSeg ((Upper_Seq C,n) /. ii),((Upper_Seq C,n) /. (ii + 1)) by A3, A4, TOPREAL1:def 5;
ii + 1 >= 1 by NAT_1:11;
then A7: ii + 1 in dom (Upper_Seq C,n) by A4, FINSEQ_3:27;
len (Gauge C,n) >= 4 by JORDAN8:13;
then ( len (Gauge C,n) = width (Gauge C,n) & len (Gauge C,n) > 1 ) by JORDAN8:def 1, XXREAL_0:2;
then A8: [i,1] in Indices (Gauge C,n) by A1, MATRIX_1:37;
ii < len (Upper_Seq C,n) by A4, NAT_1:13;
then A9: ii in dom (Upper_Seq C,n) by A3, FINSEQ_3:27;
A10: not (Gauge C,n) * i,1 in rng (Upper_Seq C,n) by A1, Th50;
Upper_Seq C,n is_sequence_on Gauge C,n by Th4;
then consider i1, j1, i2, j2 being Element of NAT such that
A11: [i1,j1] in Indices (Gauge C,n) and
A12: (Upper_Seq C,n) /. ii = (Gauge C,n) * i1,j1 and
A13: [i2,j2] in Indices (Gauge C,n) and
A14: (Upper_Seq C,n) /. (ii + 1) = (Gauge C,n) * i2,j2 and
A15: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A3, A4, JORDAN8:6;
A16: 1 <= i1 by A11, MATRIX_1:39;
A17: j2 <= width (Gauge C,n) by A13, MATRIX_1:39;
A18: 1 <= j1 by A11, MATRIX_1:39;
A19: i1 <= len (Gauge C,n) by A11, MATRIX_1:39;
A20: 1 <= j2 by A13, MATRIX_1:39;
A21: i2 <= len (Gauge C,n) by A13, MATRIX_1:39;
A22: 1 <= i2 by A13, MATRIX_1:39;
A23: j1 <= width (Gauge C,n) by A11, MATRIX_1:39;

per cases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A15;

suppose A24: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: contradiction

then j1 <= j2 by NAT_1:11;
then ((Gauge C,n) * i1,j1) `2 <= ((Gauge C,n) * i2,j2) `2 by A16, A19, A18, A17, A24, SPRECT_3:24;
then A25: ((Gauge C,n) * i1,j1) `2 <= ((Gauge C,n) * i,1) `2 by A5, A6, A12, A14, TOPREAL1:10;
((Gauge C,n) * i1,j1) `1 = ((Gauge C,n) * i2,1) `1 by A16, A19, A18, A23, A24, GOBOARD5:3
.= ((Gauge C,n) * i2,j2) `1 by A22, A21, A20, A17, GOBOARD5:3 ;
then LSeg ((Upper_Seq C,n) /. ii),((Upper_Seq C,n) /. (ii + 1)) is vertical by A12, A14, SPPOL_1:37;
then ((Gauge C,n) * i,1) `1 = ((Gauge C,n) * i1,j1) `1 by A5, A6, A12, SPPOL_1:64;
then A26: i1 = i by A11, A8, Th7;
then ((Gauge C,n) * i,1) `2 <= ((Gauge C,n) * i1,j1) `2 by A16, A19, A18, A23, SPRECT_3:24;
then j1 = 1 by A11, A8, A25, Th6, XXREAL_0:1;
hence contradiction by A12, A9, A10, A26, PARTFUN2:4; :: thesis: verum

end;

suppose A27: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: contradiction

then ((Gauge C,n) * i1,j1) `2 = ((Gauge C,n) * 1,j2) `2 by A16, A19, A18, A23, GOBOARD5:2
.= ((Gauge C,n) * i2,j2) `2 by A22, A21, A20, A17, GOBOARD5:2 ;
then LSeg ((Upper_Seq C,n) /. ii),((Upper_Seq C,n) /. (ii + 1)) is horizontal by A12, A14, SPPOL_1:36;
then ((Gauge C,n) * i,1) `2 = ((Gauge C,n) * i1,j1) `2 by A5, A6, A12, SPPOL_1:63;
then A28: j1 = 1 by A11, A8, Th6;
i2 > 1 by A16, A27, NAT_1:13;
then not (Upper_Seq C,n) /. (ii + 1) in rng (Upper_Seq C,n) by A14, A21, A27, A28, Th50;
hence contradiction by A7, PARTFUN2:4; :: thesis: verum

end;

suppose A29: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: contradiction

then ((Gauge C,n) * i1,j1) `2 = ((Gauge C,n) * 1,j2) `2 by A16, A19, A18, A23, GOBOARD5:2
.= ((Gauge C,n) * i2,j2) `2 by A22, A21, A20, A17, GOBOARD5:2 ;
then LSeg ((Upper_Seq C,n) /. ii),((Upper_Seq C,n) /. (ii + 1)) is horizontal by A12, A14, SPPOL_1:36;
then ((Gauge C,n) * i,1) `2 = ((Gauge C,n) * i1,j1) `2 by A5, A6, A12, SPPOL_1:63;
then A30: j1 = 1 by A11, A8, Th6;
i1 > 1 by A22, A29, NAT_1:13;
then not (Upper_Seq C,n) /. ii in rng (Upper_Seq C,n) by A12, A19, A30, Th50;
hence contradiction by A9, PARTFUN2:4; :: thesis: verum

end;

suppose A31: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: contradiction

then j2 <= j1 by NAT_1:11;
then ((Gauge C,n) * i2,j2) `2 <= ((Gauge C,n) * i1,j1) `2 by A16, A19, A23, A20, A31, SPRECT_3:24;
then A32: ((Gauge C,n) * i2,j2) `2 <= ((Gauge C,n) * i,1) `2 by A5, A6, A12, A14, TOPREAL1:10;
((Gauge C,n) * i1,j1) `1 = ((Gauge C,n) * i2,1) `1 by A16, A19, A18, A23, A31, GOBOARD5:3
.= ((Gauge C,n) * i2,j2) `1 by A22, A21, A20, A17, GOBOARD5:3 ;
then LSeg ((Upper_Seq C,n) /. ii),((Upper_Seq C,n) /. (ii + 1)) is vertical by A12, A14, SPPOL_1:37;
then ((Gauge C,n) * i,1) `1 = ((Gauge C,n) * i1,j1) `1 by A5, A6, A12, SPPOL_1:64;
then A33: i1 = i by A11, A8, Th7;
then ((Gauge C,n) * i,1) `2 <= ((Gauge C,n) * i2,j2) `2 by A22, A21, A20, A17, A31, SPRECT_3:24;
then j2 = 1 by A13, A8, A32, Th6, XXREAL_0:1;
hence contradiction by A14, A7, A10, A31, A33, PARTFUN2:4; :: thesis: verum

end;

end;