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,(width (Gauge C,n)) in L~ (Lower_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,(width (Gauge C,n)) in L~ (Lower_Seq C,n)
set wi = width (Gauge C,n);
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len (Gauge C,n) implies not (Gauge C,n) * i,(width (Gauge C,n)) in L~ (Lower_Seq C,n) )
assume that
A1: ( 1 <= i & i < len (Gauge C,n) ) and
A2: (Gauge C,n) * i,(width (Gauge C,n)) in L~ (Lower_Seq C,n) ; :: thesis: contradiction
set Gi1 = (Gauge C,n) * i,(width (Gauge C,n));
consider ii being Element of NAT such that
A3: ( 1 <= ii & ii + 1 <= len (Lower_Seq C,n) ) and
A4: (Gauge C,n) * i,(width (Gauge C,n)) in LSeg (Lower_Seq C,n),ii by A2, SPPOL_2:13;
A5: LSeg (Lower_Seq C,n),ii = LSeg ((Lower_Seq C,n) /. ii),((Lower_Seq C,n) /. (ii + 1)) by A3, TOPREAL1:def 5;
Lower_Seq C,n is_sequence_on Gauge C,n by Th5;
then consider i1, j1, i2, j2 being Element of NAT such that
A6: [i1,j1] in Indices (Gauge C,n) and
A7: (Lower_Seq C,n) /. ii = (Gauge C,n) * i1,j1 and
A8: [i2,j2] in Indices (Gauge C,n) and
A9: (Lower_Seq C,n) /. (ii + 1) = (Gauge C,n) * i2,j2 and
A10: ( ( 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, JORDAN8:6;
A11: ( 1 <= i1 & i1 <= len (Gauge C,n) & 1 <= j1 & j1 <= width (Gauge C,n) ) by A6, MATRIX_1:39;
A12: ( 1 <= i2 & i2 <= len (Gauge C,n) & 1 <= j2 & j2 <= width (Gauge C,n) ) by A8, MATRIX_1:39;
A13: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
len (Gauge C,n) >= 4 by JORDAN8:13;
then len (Gauge C,n) > 1 by XXREAL_0:2;
then A14: [i,(width (Gauge C,n))] in Indices (Gauge C,n) by A1, A13, MATRIX_1:37;
ii + 1 >= 1 by NAT_1:11;
then A15: ii + 1 in dom (Lower_Seq C,n) by A3, FINSEQ_3:27;
ii < len (Lower_Seq C,n) by A3, NAT_1:13;
then A16: ii in dom (Lower_Seq C,n) by A3, FINSEQ_3:27;
A17: not (Gauge C,n) * i,(width (Gauge C,n)) in rng (Lower_Seq C,n) by A1, Th51;

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

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

then ((Gauge C,n) * i1,j1) `1 = ((Gauge C,n) * i2,1) `1 by A11, GOBOARD5:3
.= ((Gauge C,n) * i2,j2) `1 by A12, GOBOARD5:3 ;
then LSeg ((Lower_Seq C,n) /. ii),((Lower_Seq C,n) /. (ii + 1)) is vertical by A7, A9, SPPOL_1:37;
then ((Gauge C,n) * i,(width (Gauge C,n))) `1 = ((Gauge C,n) * i1,j1) `1 by A4, A5, A7, SPPOL_1:64;
then A19: i1 = i by A6, A14, Th7;
j1 >= j2 by A18, NAT_1:11;
then ((Gauge C,n) * i1,j1) `2 >= ((Gauge C,n) * i2,j2) `2 by A11, A12, A18, SPRECT_3:24;
then A20: ((Gauge C,n) * i1,j1) `2 >= ((Gauge C,n) * i,(width (Gauge C,n))) `2 by A4, A5, A7, A9, TOPREAL1:10;
((Gauge C,n) * i,(width (Gauge C,n))) `2 >= ((Gauge C,n) * i1,j1) `2 by A11, A19, SPRECT_3:24;
then j1 = width (Gauge C,n) by A6, A14, A20, Th6, XXREAL_0:1;
hence contradiction by A7, A16, A17, A19, PARTFUN2:4; :: thesis: verum

end;

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

then ((Gauge C,n) * i1,j1) `2 = ((Gauge C,n) * 1,j2) `2 by A11, GOBOARD5:2
.= ((Gauge C,n) * i2,j2) `2 by A12, GOBOARD5:2 ;
then LSeg ((Lower_Seq C,n) /. ii),((Lower_Seq C,n) /. (ii + 1)) is horizontal by A7, A9, SPPOL_1:36;
then ((Gauge C,n) * i,(width (Gauge C,n))) `2 = ((Gauge C,n) * i1,j1) `2 by A4, A5, A7, SPPOL_1:63;
then A22: j1 = width (Gauge C,n) by A6, A14, Th6;
i2 < len (Gauge C,n) by A11, A21, NAT_1:13;
then not (Lower_Seq C,n) /. (ii + 1) in rng (Lower_Seq C,n) by A9, A12, A21, A22, Th51;
hence contradiction by A15, PARTFUN2:4; :: thesis: verum

end;

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

then ((Gauge C,n) * i1,j1) `2 = ((Gauge C,n) * 1,j2) `2 by A11, GOBOARD5:2
.= ((Gauge C,n) * i2,j2) `2 by A12, GOBOARD5:2 ;
then LSeg ((Lower_Seq C,n) /. ii),((Lower_Seq C,n) /. (ii + 1)) is horizontal by A7, A9, SPPOL_1:36;
then ((Gauge C,n) * i,(width (Gauge C,n))) `2 = ((Gauge C,n) * i1,j1) `2 by A4, A5, A7, SPPOL_1:63;
then A24: j1 = width (Gauge C,n) by A6, A14, Th6;
i1 < len (Gauge C,n) by A12, A23, NAT_1:13;
then not (Lower_Seq C,n) /. ii in rng (Lower_Seq C,n) by A7, A11, A24, Th51;
hence contradiction by A16, PARTFUN2:4; :: thesis: verum

end;

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

then ((Gauge C,n) * i1,j1) `1 = ((Gauge C,n) * i2,1) `1 by A11, GOBOARD5:3
.= ((Gauge C,n) * i2,j2) `1 by A12, GOBOARD5:3 ;
then LSeg ((Lower_Seq C,n) /. ii),((Lower_Seq C,n) /. (ii + 1)) is vertical by A7, A9, SPPOL_1:37;
then ((Gauge C,n) * i,(width (Gauge C,n))) `1 = ((Gauge C,n) * i1,j1) `1 by A4, A5, A7, SPPOL_1:64;
then A26: i1 = i by A6, A14, Th7;
j2 >= j1 by A25, NAT_1:11;
then ((Gauge C,n) * i2,j2) `2 >= ((Gauge C,n) * i1,j1) `2 by A11, A12, A25, SPRECT_3:24;
then A27: ((Gauge C,n) * i2,j2) `2 >= ((Gauge C,n) * i,(width (Gauge C,n))) `2 by A4, A5, A7, A9, TOPREAL1:10;
((Gauge C,n) * i,(width (Gauge C,n))) `2 >= ((Gauge C,n) * i2,j2) `2 by A12, A25, A26, SPRECT_3:24;
then j2 = width (Gauge C,n) by A8, A14, A27, Th6, XXREAL_0:1;
hence contradiction by A9, A15, A17, A25, A26, PARTFUN2:4; :: thesis: verum

end;

end;