let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for i, n, j being Element of NAT st i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
i + 1 < len (Gauge (C,n))
let i, n, j be Element of NAT ; :: thesis: ( i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C implies i + 1 < len (Gauge (C,n)) )
assume that
A1: i <= len (Gauge (C,n)) and
A2: j <= width (Gauge (C,n)) and
A3: cell ((Gauge (C,n)),i,j) c= BDD C ; :: thesis: i + 1 < len (Gauge (C,n))
A4: ( i < len (Gauge (C,n)) or i = len (Gauge (C,n)) ) by A1, XXREAL_0:1;
assume i + 1 >= len (Gauge (C,n)) ; :: thesis: contradiction
then A5: ( i + 1 > len (Gauge (C,n)) or i + 1 = len (Gauge (C,n)) ) by XXREAL_0:1;

per cases ( i = len (Gauge (C,n)) or i + 1 = len (Gauge (C,n)) ) by A5, A4, NAT_1:13;

suppose i = len (Gauge (C,n)) ; :: thesis: contradiction

hence contradiction by A2, A3, Lm5; :: thesis: verum

end;

suppose i + 1 = len (Gauge (C,n)) ; :: thesis: contradiction

then A6: cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),j) c= BDD C by A3, NAT_D:34;
BDD C c= C ` by JORDAN2C:29;
then A7: cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),j) c= C ` by A6, XBOOLE_1:1;
A8: len (Gauge (C,n)) <> 0 by GOBOARD1:def 5;
then A9: ((len (Gauge (C,n))) -' 1) + 1 = len (Gauge (C,n)) by NAT_1:14, XREAL_1:237;
(len (Gauge (C,n))) -' 1 <= len (Gauge (C,n)) by NAT_D:44;
then A10: not cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),j) is empty by A2, JORDAN1A:45;
A11: j <> 0 by A1, A3, Lm4;
UBD C is_outside_component_of C by JORDAN2C:73, JORDAN2C:76;
then A12: UBD C is_a_component_of C ` by JORDAN2C:def 4;
len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
then A13: cell ((Gauge (C,n)),(len (Gauge (C,n))),j) c= UBD C by A2, Th39;
A14: (len (Gauge (C,n))) - 1 < len (Gauge (C,n)) by XREAL_1:148;
j < width (Gauge (C,n)) by A1, A2, A3, Lm6, XXREAL_0:1;
then (cell ((Gauge (C,n)),(len (Gauge (C,n))),j)) /\ (cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),j)) = LSeg (((Gauge (C,n)) * ((len (Gauge (C,n))),j)),((Gauge (C,n)) * ((len (Gauge (C,n))),(j + 1)))) by A14, A9, A11, GOBOARD5:26, NAT_1:14;
then A15: cell ((Gauge (C,n)),(len (Gauge (C,n))),j) meets cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),j) by XBOOLE_0:def 7;
(len (Gauge (C,n))) -' 1 < len (Gauge (C,n)) by A8, A14, NAT_1:14, XREAL_1:235;
then cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),j) c= UBD C by A2, A13, A15, A12, A7, GOBOARD9:6, JORDAN1A:46;
hence contradiction by A6, A10, JORDAN2C:28, XBOOLE_1:68; :: thesis: verum

end;

end;