let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Nat ex i being 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 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)) )
set G = Gauge (C,n);
defpred S1[ Nat] means ( 1 <= $1 & $1 < len (Gauge (C,n)) & ((Gauge (C,n)) * ($1,((width (Gauge (C,n))) -' 1))) `1 < (N-min C) `1 );
A1: for k being Nat st S1[k] holds
k <= len (Gauge (C,n)) ;
A2: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
(NW-corner C) `1 <= (N-min C) `1 by PSCOMP_1:38;
then A3: W-bound C <= (N-min C) `1 by EUCLID:52;
A4: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A5: ( (len (Gauge (C,n))) -' 1 <= len (Gauge (C,n)) & 2 <= len (Gauge (C,n)) ) by NAT_D:35, XXREAL_0:2;
A6: 1 < len (Gauge (C,n)) by A4, XXREAL_0:2;
then A7: 1 <= (len (Gauge (C,n))) -' 1 by NAT_D:49;
A8: ( n in NAT & len (Gauge (C,n)) = width (Gauge (C,n)) ) by JORDAN8:def 1, ORDINAL1:def 12;
then ((Gauge (C,n)) * (2,((width (Gauge (C,n))) -' 1))) `1 = W-bound C by A7, JORDAN8:11, NAT_D:35;
then ((Gauge (C,n)) * (1,((width (Gauge (C,n))) -' 1))) `1 < W-bound C by A2, A7, A5, GOBOARD5:3;
then ((Gauge (C,n)) * (1,((width (Gauge (C,n))) -' 1))) `1 < (N-min C) `1 by A3, XXREAL_0:2;
then A9: ex k being Nat st S1[k] by A6;
ex i being Nat st
( S1[i] & ( for n being Nat st S1[n] holds
n <= i ) ) from NAT_1:sch 6(A1, A9);
 then consider i being Nat such that
A10: 1 <= i and
A11: i < len (Gauge (C,n)) and
A12: ((Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1))) `1 < (N-min C) `1 and
A13: for n being Nat st S1[n] holds
n <= i ;
reconsider i = i as Nat ;
A14: ( 1 <= i + 1 & i < i + 1 ) by NAT_1:12, NAT_1:13;
A15: (N-min C) `2 = N-bound C by EUCLID:52;
A16: i + 1 <= len (Gauge (C,n)) by A11, NAT_1:13;
then A17: (N-min C) `2 = ((Gauge (C,n)) * ((i + 1),((width (Gauge (C,n))) -' 1))) `2 by A8, A15, JORDAN8:14, NAT_1:12;
now :: thesis: not i + 1 = len (Gauge (C,n))
assume i + 1 = len (Gauge (C,n)) ; :: thesis: contradiction
then (len (Gauge (C,n))) -' 1 = i by NAT_D:34;
then A18: ((Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1))) `1 = E-bound C by A8, A7, JORDAN8:12, NAT_D:35;
(NE-corner C) `1 >= (N-min C) `1 by PSCOMP_1:38;
hence contradiction by A12, A18, EUCLID:52; :: thesis: verum
end;
then i + 1 < len (Gauge (C,n)) by A16, XXREAL_0:1;
then A19: (N-min C) `1 <= ((Gauge (C,n)) * ((i + 1),((width (Gauge (C,n))) -' 1))) `1 by A13, A14;
((Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1))) `2 = (N-min C) `2 by A8, A10, A11, A15, JORDAN8:14;
then A20: 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 A12, A17, A19, GOBOARD7:8;
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 A10, A11, 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)) )
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 A2, A7, A10, A11, GOBOARD5:22, NAT_D:35;
hence N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) by A20; :: 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 A12; :: thesis: verum