let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Nat ex i being Element of NAT st
( 1 <= i & i + 1 <= len (Gauge C,n) & N-min C in cell (Gauge C,n),i,((width (Gauge C,n)) -' 1) & N-min C <> (Gauge C,n) * i,((width (Gauge C,n)) -' 1) )
let n be Nat; :: thesis: ex i being Element of NAT st
( 1 <= i & i + 1 <= len (Gauge C,n) & N-min C in cell (Gauge C,n),i,((width (Gauge C,n)) -' 1) & N-min C <> (Gauge C,n) * i,((width (Gauge C,n)) -' 1) )
A1: n in NAT by ORDINAL1:def 13;
set G = Gauge C,n;
A2: 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) * $1,((width (Gauge C,n)) -' 1)) `1 < (N-min C) `1 );
A3: for k being Nat st S₁[k] holds
k <= len (Gauge C,n) ;
A4: ( len (Gauge C,n) = (2 |^ n) + 3 & len (Gauge C,n) = width (Gauge C,n) ) by JORDAN8:def 1;
A5: len (Gauge C,n) >= 4 by JORDAN8:13;
then A6: 1 < len (Gauge C,n) by XXREAL_0:2;
then A7: 1 <= (len (Gauge C,n)) -' 1 by NAT_D:49;
A8: (len (Gauge C,n)) -' 1 <= len (Gauge C,n) by NAT_D:35;
(NW-corner C) `1 <= (N-min C) `1 by PSCOMP_1:97;
then A9: W-bound C <= (N-min C) `1 by EUCLID:56;
A10: 2 <= len (Gauge C,n) by A5, XXREAL_0:2;
((Gauge C,n) * 2,((width (Gauge C,n)) -' 1)) `1 = W-bound C by A1, A2, A7, JORDAN8:14, NAT_D:35;
then ((Gauge C,n) * 1,((width (Gauge C,n)) -' 1)) `1 < W-bound C by A4, A7, A8, A10, GOBOARD5:4;
then ((Gauge C,n) * 1,((width (Gauge C,n)) -' 1)) `1 < (N-min C) `1 by A9, XXREAL_0:2;
then A11: ex k being Nat st S<sub>1</sub>[k] by A6;
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(A3, A11);
then consider i being Nat such that
A12: ( 1 <= i & i < len (Gauge C,n) ) and
A13: ((Gauge C,n) * i,((width (Gauge C,n)) -' 1)) `1 < (N-min C) `1 and
A14: 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) & N-min C in cell (Gauge C,n),i,((width (Gauge C,n)) -' 1) & N-min C <> (Gauge C,n) * i,((width (Gauge C,n)) -' 1) )
thus ( 1 <= i & i + 1 <= len (Gauge C,n) ) by A12, NAT_1:13; :: thesis: ( N-min C in cell (Gauge C,n),i,((width (Gauge C,n)) -' 1) & N-min C <> (Gauge C,n) * i,((width (Gauge C,n)) -' 1) )
A15: LSeg ((Gauge C,n) * i,((width (Gauge C,n)) -' 1)),((Gauge C,n) * (i + 1),((width (Gauge C,n)) -' 1)) c= cell (Gauge C,n),i,((width (Gauge C,n)) -' 1) by A4, A7, A12, GOBOARD5:23, NAT_D:35;
A16: i + 1 <= len (Gauge C,n) by A12, NAT_1:13;
A17: 1 <= i + 1 by NAT_1:12;
(N-min C) `2 = N-bound C by EUCLID:56;
then A18: ( ((Gauge C,n) * i,((width (Gauge C,n)) -' 1)) `2 = (N-min C) `2 & (N-min C) `2 = ((Gauge C,n) * (i + 1),((width (Gauge C,n)) -' 1)) `2 ) by A1, A2, A12, A16, JORDAN8:17, 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 A19: ((Gauge C,n) * i,((width (Gauge C,n)) -' 1)) `1 = E-bound C by A1, A2, A7, JORDAN8:15, NAT_D:35;
(NE-corner C) `1 >= (N-min C) `1 by PSCOMP_1:97;
hence contradiction by A13, A19, EUCLID:56; :: thesis: verum

end;

then ( i + 1 < len (Gauge C,n) & i < i + 1 ) by A16, NAT_1:13, XXREAL_0:1;
then (N-min C) `1 <= ((Gauge C,n) * (i + 1),((width (Gauge C,n)) -' 1)) `1 by A14, A17;
then N-min C in LSeg ((Gauge C,n) * i,((width (Gauge C,n)) -' 1)),((Gauge C,n) * (i + 1),((width (Gauge C,n)) -' 1)) by A13, A18, GOBOARD7:9;
hence N-min C in cell (Gauge C,n),i,((width (Gauge C,n)) -' 1) by A15; :: thesis: N-min C <> (Gauge C,n) * i,((width (Gauge C,n)) -' 1)
thus N-min C <> (Gauge C,n) * i,((width (Gauge C,n)) -' 1) by A13; :: thesis: verum