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 < 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); :: thesis: for i, j, k being Element of 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 Element of NAT ; :: thesis: ( 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 & i < len (Gauge C,n) )
and
A2:
( 1 <= j & k <= width (Gauge C,n) )
and
A3:
(Gauge C,n) * i,k in L~ (Upper_Seq C,n)
and
A4:
(Gauge C,n) * i,j in L~ (Lower_Seq C,n)
and
A5:
j = k
; :: thesis: contradiction
A6:
len (Gauge C,n) = width (Gauge C,n)
by JORDAN8:def 1;
(Gauge C,n) * i,k in (L~ (Upper_Seq C,n)) /\ (L~ (Lower_Seq C,n))
by A3, A4, A5, XBOOLE_0:def 4;
then A7:
(Gauge C,n) * i,k in {(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))}
by JORDAN1E:20;
A8:
[i,j] in Indices (Gauge C,n)
by A1, A2, A5, MATRIX_1:37;
len (Gauge C,n) >= 4
by JORDAN8:13;
then A9:
len (Gauge C,n) >= 1
by XXREAL_0:2;
then A10:
[(len (Gauge C,n)),j] in Indices (Gauge C,n)
by A2, A5, MATRIX_1:37;
A11:
[1,j] in Indices (Gauge C,n)
by A2, A5, A9, MATRIX_1:37;
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 A7, TARSKI:def 2;
suppose A12:
(Gauge C,n) * i,
k = W-min (L~ (Cage C,n))
;
:: thesis: contradiction
((Gauge C,n) * 1,j) `1 = W-bound (L~ (Cage C,n))
by A2, A5, A6, JORDAN1A:94;
then
(W-min (L~ (Cage C,n))) `1 <> W-bound (L~ (Cage C,n))
by A1, A5, A8, A11, A12, JORDAN1G:7;
hence
contradiction
by EUCLID:56;
:: thesis: verum end; suppose A13:
(Gauge C,n) * i,
k = E-max (L~ (Cage C,n))
;
:: thesis: contradiction
((Gauge C,n) * (len (Gauge C,n)),j) `1 = E-bound (L~ (Cage C,n))
by A2, A5, A6, JORDAN1A:92;
then
(E-max (L~ (Cage C,n))) `1 <> E-bound (L~ (Cage C,n))
by A1, A5, A8, A10, A13, JORDAN1G:7;
hence
contradiction
by EUCLID:56;
:: thesis: verum end;