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