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;