let n be Element of NAT ; :: thesis: for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i + 1 <= len (Gauge C,n) & W-min C in cell (Gauge C,n),1,i & W-min C <> (Gauge C,n) * 2,i )
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ex i being Element of NAT st
( 1 <= i & i + 1 <= len (Gauge C,n) & W-min C in cell (Gauge C,n),1,i & W-min C <> (Gauge C,n) * 2,i )
set G = Gauge C,n;
A1: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
defpred S₁[ Nat] means ( 1 <= $1 & $1 < len (Gauge C,n) & ((Gauge C,n) * 2,$1) `2 < (W-min C) `2 );
A2: for k being Nat st S₁[k] holds
k <= len (Gauge C,n) ;
A3: ( len (Gauge C,n) = (2 |^ n) + 3 & len (Gauge C,n) = width (Gauge C,n) ) by JORDAN8:def 1;
A4: len (Gauge C,n) >= 4 by JORDAN8:13;
then A5: 1 < len (Gauge C,n) by XXREAL_0:2;
(SW-corner C) `2 <= (W-min C) `2 by PSCOMP_1:87;
then A6: S-bound C <= (W-min C) `2 by EUCLID:56;
A7: 2 <= len (Gauge C,n) by A4, XXREAL_0:2;
then ((Gauge C,n) * 2,2) `2 = S-bound C by JORDAN8:16;
then ((Gauge C,n) * 2,1) `2 < S-bound C by A3, A7, GOBOARD5:5;
then ((Gauge C,n) * 2,1) `2 < (W-min C) `2 by A6, XXREAL_0:2;
then A8: ex k being Nat st S<sub>1</sub>[k] by A5;
ex i being Nat st
( S<sub>1</sub>[i] & ( for n being Nat st S<sub>1</sub>[n] holds
n <= i ) ) from NAT_1:sch 6(A2, A8);
then consider i being Nat such that
A9: ( 1 <= i & i < len (Gauge C,n) ) and
A10: ((Gauge C,n) * 2,i) `2 < (W-min C) `2 and
A11: for n being Nat st S<sub>1</sub>[n] holds
n <= i ;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
take i ; :: thesis: ( 1 <= i & i + 1 <= len (Gauge C,n) & W-min C in cell (Gauge C,n),1,i & W-min C <> (Gauge C,n) * 2,i )
thus ( 1 <= i & i + 1 <= len (Gauge C,n) ) by A9, NAT_1:13; :: thesis: ( W-min C in cell (Gauge C,n),1,i & W-min C <> (Gauge C,n) * 2,i )
A12: LSeg ((Gauge C,n) * (1 + 1),i),((Gauge C,n) * (1 + 1),(i + 1)) c= cell (Gauge C,n),1,i by A1, A5, A9, GOBOARD5:19;
A13: i + 1 <= len (Gauge C,n) by A9, NAT_1:13;
A14: 1 <= i + 1 by NAT_1:12;
(W-min C) `1 = W-bound C by EUCLID:56;
then A15: ( ((Gauge C,n) * 2,i) `1 = (W-min C) `1 & (W-min C) `1 = ((Gauge C,n) * 2,(i + 1)) `1 ) by A9, A13, JORDAN8:14, NAT_1:12;

now

assume i + 1 = len (Gauge C,n) ; :: thesis: contradiction
then (len (Gauge C,n)) -' 1 = i by NAT_D:34;
then A16: ((Gauge C,n) * 2,i) `2 = N-bound C by A7, JORDAN8:17;
(NW-corner C) `2 >= (W-min C) `2 by PSCOMP_1:87;
hence contradiction by A10, A16, EUCLID:56; :: thesis: verum

end;

then ( i + 1 < len (Gauge C,n) & i < i + 1 ) by A13, NAT_1:13, XXREAL_0:1;
then (W-min C) `2 <= ((Gauge C,n) * 2,(i + 1)) `2 by A11, A14;
then W-min C in LSeg ((Gauge C,n) * 2,i),((Gauge C,n) * 2,(i + 1)) by A10, A15, GOBOARD7:8;
hence W-min C in cell (Gauge C,n),1,i by A12; :: thesis: W-min C <> (Gauge C,n) * 2,i
thus W-min C <> (Gauge C,n) * 2,i by A10; :: thesis: verum