let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of ()
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 (); :: 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 ;
(Gauge (C,n)) * (k,i) in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) by ;
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 ;
A13: [1,i] in Indices (Gauge (C,n)) by ;
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 ;
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 ;
then (W-min (L~ (Cage (C,n)))) `1 <> W-bound (L~ (Cage (C,n))) by ;
hence contradiction by EUCLID:52; :: 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 ;
then (E-max (L~ (Cage (C,n)))) `1 <> E-bound (L~ (Cage (C,n))) by ;
hence contradiction by EUCLID:52; :: thesis: verum
end;
end;