let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Element of 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 Element of 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 Element of 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_1:37;
(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:20;
A10: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
len (Gauge C,n) >= 4 by JORDAN8:13;
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_1:37;
A13: [1,i] in Indices (Gauge C,n) by A3, A4, A11, MATRIX_1:37;

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;

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:94;
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:56; :: thesis: verum

end;

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:92;
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:56; :: thesis: verum

end;

end;