let n be Nat; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= j & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) holds
j <> k
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= j & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) holds
j <> k
let i, j, k be Nat; ( 1 < i & i < len (Gauge (C,n)) & 1 <= j & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) implies j <> k )
assume that
A1:
1 < i
and
A2:
i < len (Gauge (C,n))
and
A3:
1 <= j
and
A4:
k <= width (Gauge (C,n))
and
A5:
(Gauge (C,n)) * (i,k) in L~ (Upper_Seq (C,n))
and
A6:
(Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n))
and
A7:
j = k
; contradiction
A8:
[i,j] in Indices (Gauge (C,n))
by A1, A2, A3, A4, A7, MATRIX_0:30;
(Gauge (C,n)) * (i,k) in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n)))
by A5, A6, A7, XBOOLE_0:def 4;
then A9:
(Gauge (C,n)) * (i,k) 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))),j] in Indices (Gauge (C,n))
by A3, A4, A7, MATRIX_0:30;
A13:
[1,j] in Indices (Gauge (C,n))
by A3, A4, A7, A11, MATRIX_0:30;
per cases
( (Gauge (C,n)) * (i,k) = W-min (L~ (Cage (C,n))) or (Gauge (C,n)) * (i,k) = E-max (L~ (Cage (C,n))) )
by A9, TARSKI:def 2;
suppose A14:
(Gauge (C,n)) * (
i,
k)
= W-min (L~ (Cage (C,n)))
;
contradiction
((Gauge (C,n)) * (1,j)) `1 = W-bound (L~ (Cage (C,n)))
by A3, A4, A7, 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;
verum end; suppose A15:
(Gauge (C,n)) * (
i,
k)
= E-max (L~ (Cage (C,n)))
;
contradiction
((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 = E-bound (L~ (Cage (C,n)))
by A3, A4, A7, 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;
verum end; end;