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
j + 1 < width (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 j + 1 < width (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: j + 1 < width (Gauge C,n)
assume j + 1 >= width (Gauge C,n) ; :: thesis: contradiction
then A4: ( j + 1 > width (Gauge C,n) or j + 1 = width (Gauge C,n) ) by XXREAL_0:1;
A5: ( j < width (Gauge C,n) or j = width (Gauge C,n) ) by A2, XXREAL_0:1;

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

suppose j = width (Gauge C,n) ; :: thesis: contradiction

hence contradiction by A1, A3, Lm6; :: thesis: verum

end;

suppose j + 1 = width (Gauge C,n) ; :: thesis: contradiction

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

end;

end;