let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for i, j, n being 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, j, n be 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:25;
then A7: cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),j) c= C ` by A6;
A8: len (Gauge (C,n)) <> 0 by MATRIX_0:def 10;
then A9: ((len (Gauge (C,n))) -' 1) + 1 = len (Gauge (C,n)) by NAT_1:14, XREAL_1:235;
(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:24;
A11: j <> 0 by A1, A3, Lm4;
UBD C is_outside_component_of C by JORDAN2C:68;
then A12: UBD C is_a_component_of C ` by JORDAN2C:def 3;
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, Th36;
A14: (len (Gauge (C,n))) - 1 < len (Gauge (C,n)) by XREAL_1:146;
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:25, 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:233;
then cell ((Gauge (C,n)),((len (Gauge (C,n))) -' 1),j) c= UBD C by A2, A13, A15, A12, A7, GOBOARD9:4, JORDAN1A:25;
hence contradiction by A6, A10, JORDAN2C:24, XBOOLE_1:68; :: thesis: verum

end;

end;