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

for i, j, k being Nat st 1 < j & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Lower_Seq (C,n)) holds

j <> k

let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for i, j, k being Nat st 1 < j & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Lower_Seq (C,n)) holds

j <> k

let i, j, k be Nat; :: thesis: ( 1 < j & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Lower_Seq (C,n)) implies j <> k )

assume that

A1: 1 < j and

A2: k < len (Gauge (C,n)) and

A3: 1 <= i and

A4: i <= width (Gauge (C,n)) and

A5: (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) and

A6: (Gauge (C,n)) * (j,i) in L~ (Lower_Seq (C,n)) and

A7: j = k ; :: thesis: contradiction

A8: [j,i] in Indices (Gauge (C,n)) by A1, A2, A3, A4, A7, MATRIX_0:30;

(Gauge (C,n)) * (k,i) in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) by A5, A6, A7, XBOOLE_0:def 4;

then A9: (Gauge (C,n)) * (k,i) in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} by JORDAN1E:16;

A10: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;

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

then A11: len (Gauge (C,n)) >= 1 by XXREAL_0:2;

then A12: [(len (Gauge (C,n))),i] in Indices (Gauge (C,n)) by A3, A4, MATRIX_0:30;

A13: [1,i] in Indices (Gauge (C,n)) by A3, A4, A11, MATRIX_0:30;

for i, j, k being Nat st 1 < j & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Lower_Seq (C,n)) holds

j <> k

let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for i, j, k being Nat st 1 < j & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Lower_Seq (C,n)) holds

j <> k

let i, j, k be Nat; :: thesis: ( 1 < j & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (j,i) in L~ (Lower_Seq (C,n)) implies j <> k )

assume that

A1: 1 < j and

A2: k < len (Gauge (C,n)) and

A3: 1 <= i and

A4: i <= width (Gauge (C,n)) and

A5: (Gauge (C,n)) * (k,i) in L~ (Upper_Seq (C,n)) and

A6: (Gauge (C,n)) * (j,i) in L~ (Lower_Seq (C,n)) and

A7: j = k ; :: thesis: contradiction

A8: [j,i] in Indices (Gauge (C,n)) by A1, A2, A3, A4, A7, MATRIX_0:30;

(Gauge (C,n)) * (k,i) in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) by A5, A6, A7, XBOOLE_0:def 4;

then A9: (Gauge (C,n)) * (k,i) in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} by JORDAN1E:16;

A10: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;

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

then A11: len (Gauge (C,n)) >= 1 by XXREAL_0:2;

then A12: [(len (Gauge (C,n))),i] in Indices (Gauge (C,n)) by A3, A4, MATRIX_0:30;

A13: [1,i] in Indices (Gauge (C,n)) by A3, A4, A11, MATRIX_0:30;

per cases
( (Gauge (C,n)) * (k,i) = W-min (L~ (Cage (C,n))) or (Gauge (C,n)) * (k,i) = E-max (L~ (Cage (C,n))) )
by A9, TARSKI:def 2;

end;

suppose A14:
(Gauge (C,n)) * (k,i) = W-min (L~ (Cage (C,n)))
; :: thesis: contradiction

((Gauge (C,n)) * (1,i)) `1 = W-bound (L~ (Cage (C,n)))
by A3, A4, A10, JORDAN1A:73;

then (W-min (L~ (Cage (C,n)))) `1 <> W-bound (L~ (Cage (C,n))) by A1, A7, A8, A13, A14, JORDAN1G:7;

hence contradiction by EUCLID:52; :: thesis: verum

end;then (W-min (L~ (Cage (C,n)))) `1 <> W-bound (L~ (Cage (C,n))) by A1, A7, A8, A13, A14, JORDAN1G:7;

hence contradiction by EUCLID:52; :: thesis: verum

suppose A15:
(Gauge (C,n)) * (k,i) = E-max (L~ (Cage (C,n)))
; :: thesis: contradiction

((Gauge (C,n)) * ((len (Gauge (C,n))),i)) `1 = E-bound (L~ (Cage (C,n)))
by A3, A4, A10, JORDAN1A:71;

then (E-max (L~ (Cage (C,n)))) `1 <> E-bound (L~ (Cage (C,n))) by A2, A7, A8, A12, A15, JORDAN1G:7;

hence contradiction by EUCLID:52; :: thesis: verum

end;then (E-max (L~ (Cage (C,n)))) `1 <> E-bound (L~ (Cage (C,n))) by A2, A7, A8, A12, A15, JORDAN1G:7;

hence contradiction by EUCLID:52; :: thesis: verum