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 < 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); 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; ( 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
; 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;
suppose A14:
(Gauge (C,n)) * (
k,
i)
= W-min (L~ (Cage (C,n)))
;
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;
verum end; suppose A15:
(Gauge (C,n)) * (
k,
i)
= E-max (L~ (Cage (C,n)))
;
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;
verum end;