let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for i being 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 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 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 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 3;

ii + 1 >= 1 by NAT_1:11;

then A7: ii + 1 in dom (Upper_Seq (C,n)) by A4, FINSEQ_3:25;

len (Gauge (C,n)) >= 4 by JORDAN8:10;

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_0:30;

ii < len (Upper_Seq (C,n)) by A4, NAT_1:13;

then A9: ii in dom (Upper_Seq (C,n)) by A3, FINSEQ_3:25;

A10: not (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n)) by A1, Th42;

Upper_Seq (C,n) is_sequence_on Gauge (C,n) by Th4;

then consider i1, j1, i2, j2 being 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:3;

A16: 1 <= i1 by A11, MATRIX_0:32;

A17: j2 <= width (Gauge (C,n)) by A13, MATRIX_0:32;

A18: 1 <= j1 by A11, MATRIX_0:32;

A19: i1 <= len (Gauge (C,n)) by A11, MATRIX_0:32;

A20: 1 <= j2 by A13, MATRIX_0:32;

A21: i2 <= len (Gauge (C,n)) by A13, MATRIX_0:32;

A22: 1 <= i2 by A13, MATRIX_0:32;

A23: j1 <= width (Gauge (C,n)) by A11, MATRIX_0:32;

for i being 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 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 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 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 3;

ii + 1 >= 1 by NAT_1:11;

then A7: ii + 1 in dom (Upper_Seq (C,n)) by A4, FINSEQ_3:25;

len (Gauge (C,n)) >= 4 by JORDAN8:10;

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_0:30;

ii < len (Upper_Seq (C,n)) by A4, NAT_1:13;

then A9: ii in dom (Upper_Seq (C,n)) by A3, FINSEQ_3:25;

A10: not (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n)) by A1, Th42;

Upper_Seq (C,n) is_sequence_on Gauge (C,n) by Th4;

then consider i1, j1, i2, j2 being 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:3;

A16: 1 <= i1 by A11, MATRIX_0:32;

A17: j2 <= width (Gauge (C,n)) by A13, MATRIX_0:32;

A18: 1 <= j1 by A11, MATRIX_0:32;

A19: i1 <= len (Gauge (C,n)) by A11, MATRIX_0:32;

A20: 1 <= j2 by A13, MATRIX_0:32;

A21: i2 <= len (Gauge (C,n)) by A13, MATRIX_0:32;

A22: 1 <= i2 by A13, MATRIX_0:32;

A23: j1 <= width (Gauge (C,n)) by A11, MATRIX_0:32;

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;

end;

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:12;

then A25: ((Gauge (C,n)) * (i1,j1)) `2 <= ((Gauge (C,n)) * (i,1)) `2 by A5, A6, A12, A14, TOPREAL1:4;

((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * (i2,1)) `1 by A16, A19, A18, A23, A24, GOBOARD5:2

.= ((Gauge (C,n)) * (i2,j2)) `1 by A22, A21, A20, A17, GOBOARD5:2 ;

then LSeg (((Upper_Seq (C,n)) /. ii),((Upper_Seq (C,n)) /. (ii + 1))) is vertical by A12, A14, SPPOL_1:16;

then ((Gauge (C,n)) * (i,1)) `1 = ((Gauge (C,n)) * (i1,j1)) `1 by A5, A6, A12, SPPOL_1:41;

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:12;

then j1 = 1 by A11, A8, A25, Th6, XXREAL_0:1;

hence contradiction by A12, A9, A10, A26, PARTFUN2:2; :: thesis: verum

end;then ((Gauge (C,n)) * (i1,j1)) `2 <= ((Gauge (C,n)) * (i2,j2)) `2 by A16, A19, A18, A17, A24, SPRECT_3:12;

then A25: ((Gauge (C,n)) * (i1,j1)) `2 <= ((Gauge (C,n)) * (i,1)) `2 by A5, A6, A12, A14, TOPREAL1:4;

((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * (i2,1)) `1 by A16, A19, A18, A23, A24, GOBOARD5:2

.= ((Gauge (C,n)) * (i2,j2)) `1 by A22, A21, A20, A17, GOBOARD5:2 ;

then LSeg (((Upper_Seq (C,n)) /. ii),((Upper_Seq (C,n)) /. (ii + 1))) is vertical by A12, A14, SPPOL_1:16;

then ((Gauge (C,n)) * (i,1)) `1 = ((Gauge (C,n)) * (i1,j1)) `1 by A5, A6, A12, SPPOL_1:41;

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:12;

then j1 = 1 by A11, A8, A25, Th6, XXREAL_0:1;

hence contradiction by A12, A9, A10, A26, PARTFUN2:2; :: thesis: verum

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:1

.= ((Gauge (C,n)) * (i2,j2)) `2 by A22, A21, A20, A17, GOBOARD5:1 ;

then LSeg (((Upper_Seq (C,n)) /. ii),((Upper_Seq (C,n)) /. (ii + 1))) is horizontal by A12, A14, SPPOL_1:15;

then ((Gauge (C,n)) * (i,1)) `2 = ((Gauge (C,n)) * (i1,j1)) `2 by A5, A6, A12, SPPOL_1:40;

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, Th42;

hence contradiction by A7, PARTFUN2:2; :: thesis: verum

end;.= ((Gauge (C,n)) * (i2,j2)) `2 by A22, A21, A20, A17, GOBOARD5:1 ;

then LSeg (((Upper_Seq (C,n)) /. ii),((Upper_Seq (C,n)) /. (ii + 1))) is horizontal by A12, A14, SPPOL_1:15;

then ((Gauge (C,n)) * (i,1)) `2 = ((Gauge (C,n)) * (i1,j1)) `2 by A5, A6, A12, SPPOL_1:40;

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, Th42;

hence contradiction by A7, PARTFUN2:2; :: thesis: verum

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:1

.= ((Gauge (C,n)) * (i2,j2)) `2 by A22, A21, A20, A17, GOBOARD5:1 ;

then LSeg (((Upper_Seq (C,n)) /. ii),((Upper_Seq (C,n)) /. (ii + 1))) is horizontal by A12, A14, SPPOL_1:15;

then ((Gauge (C,n)) * (i,1)) `2 = ((Gauge (C,n)) * (i1,j1)) `2 by A5, A6, A12, SPPOL_1:40;

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, Th42;

hence contradiction by A9, PARTFUN2:2; :: thesis: verum

end;.= ((Gauge (C,n)) * (i2,j2)) `2 by A22, A21, A20, A17, GOBOARD5:1 ;

then LSeg (((Upper_Seq (C,n)) /. ii),((Upper_Seq (C,n)) /. (ii + 1))) is horizontal by A12, A14, SPPOL_1:15;

then ((Gauge (C,n)) * (i,1)) `2 = ((Gauge (C,n)) * (i1,j1)) `2 by A5, A6, A12, SPPOL_1:40;

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, Th42;

hence contradiction by A9, PARTFUN2:2; :: thesis: verum

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:12;

then A32: ((Gauge (C,n)) * (i2,j2)) `2 <= ((Gauge (C,n)) * (i,1)) `2 by A5, A6, A12, A14, TOPREAL1:4;

((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * (i2,1)) `1 by A16, A19, A18, A23, A31, GOBOARD5:2

.= ((Gauge (C,n)) * (i2,j2)) `1 by A22, A21, A20, A17, GOBOARD5:2 ;

then LSeg (((Upper_Seq (C,n)) /. ii),((Upper_Seq (C,n)) /. (ii + 1))) is vertical by A12, A14, SPPOL_1:16;

then ((Gauge (C,n)) * (i,1)) `1 = ((Gauge (C,n)) * (i1,j1)) `1 by A5, A6, A12, SPPOL_1:41;

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:12;

then j2 = 1 by A13, A8, A32, Th6, XXREAL_0:1;

hence contradiction by A14, A7, A10, A31, A33, PARTFUN2:2; :: thesis: verum

end;then ((Gauge (C,n)) * (i2,j2)) `2 <= ((Gauge (C,n)) * (i1,j1)) `2 by A16, A19, A23, A20, A31, SPRECT_3:12;

then A32: ((Gauge (C,n)) * (i2,j2)) `2 <= ((Gauge (C,n)) * (i,1)) `2 by A5, A6, A12, A14, TOPREAL1:4;

((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * (i2,1)) `1 by A16, A19, A18, A23, A31, GOBOARD5:2

.= ((Gauge (C,n)) * (i2,j2)) `1 by A22, A21, A20, A17, GOBOARD5:2 ;

then LSeg (((Upper_Seq (C,n)) /. ii),((Upper_Seq (C,n)) /. (ii + 1))) is vertical by A12, A14, SPPOL_1:16;

then ((Gauge (C,n)) * (i,1)) `1 = ((Gauge (C,n)) * (i1,j1)) `1 by A5, A6, A12, SPPOL_1:41;

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:12;

then j2 = 1 by A13, A8, A32, Th6, XXREAL_0:1;

hence contradiction by A14, A7, A10, A31, A33, PARTFUN2:2; :: thesis: verum