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

j + 1 < width (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 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))

A4: ( j < width (Gauge (C,n)) or j = width (Gauge (C,n)) ) by A2, XXREAL_0:1;

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

then A5: ( j + 1 > width (Gauge (C,n)) or j + 1 = width (Gauge (C,n)) ) by XXREAL_0:1;

j + 1 < width (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 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))

A4: ( j < width (Gauge (C,n)) or j = width (Gauge (C,n)) ) by A2, XXREAL_0:1;

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

then A5: ( j + 1 > width (Gauge (C,n)) or j + 1 = width (Gauge (C,n)) ) by XXREAL_0:1;

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

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;

BDD C c= C ` by JORDAN2C:25;

then A7: cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) c= C ` by A6;

A8: width (Gauge (C,n)) <> 0 by MATRIX_0:def 10;

then A9: ((width (Gauge (C,n))) -' 1) + 1 = width (Gauge (C,n)) by NAT_1:14, XREAL_1:235;

(width (Gauge (C,n))) -' 1 <= width (Gauge (C,n)) by NAT_D:44;

then A10: not cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) is empty by A1, JORDAN1A:24;

A11: cell ((Gauge (C,n)),i,(width (Gauge (C,n)))) c= UBD C by A1, JORDAN1A:50;

UBD C is_outside_component_of C by JORDAN2C:68;

then A12: UBD C is_a_component_of C ` by JORDAN2C:def 3;

A13: i <> 0 by A2, A3, Lm3;

A14: (width (Gauge (C,n))) - 1 < width (Gauge (C,n)) by XREAL_1:146;

i < len (Gauge (C,n)) by A1, A2, A3, Lm5, XXREAL_0:1;

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 A14, A9, A13, GOBOARD5:26, NAT_1:14;

then A15: 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;

(width (Gauge (C,n))) -' 1 < width (Gauge (C,n)) by A8, A14, NAT_1:14, XREAL_1:233;

then cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) c= UBD C by A1, A11, A15, A12, A7, GOBOARD9:4, JORDAN1A:25;

hence contradiction by A6, A10, JORDAN2C:24, XBOOLE_1:68; :: thesis: verum

end;BDD C c= C ` by JORDAN2C:25;

then A7: cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) c= C ` by A6;

A8: width (Gauge (C,n)) <> 0 by MATRIX_0:def 10;

then A9: ((width (Gauge (C,n))) -' 1) + 1 = width (Gauge (C,n)) by NAT_1:14, XREAL_1:235;

(width (Gauge (C,n))) -' 1 <= width (Gauge (C,n)) by NAT_D:44;

then A10: not cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) is empty by A1, JORDAN1A:24;

A11: cell ((Gauge (C,n)),i,(width (Gauge (C,n)))) c= UBD C by A1, JORDAN1A:50;

UBD C is_outside_component_of C by JORDAN2C:68;

then A12: UBD C is_a_component_of C ` by JORDAN2C:def 3;

A13: i <> 0 by A2, A3, Lm3;

A14: (width (Gauge (C,n))) - 1 < width (Gauge (C,n)) by XREAL_1:146;

i < len (Gauge (C,n)) by A1, A2, A3, Lm5, XXREAL_0:1;

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 A14, A9, A13, GOBOARD5:26, NAT_1:14;

then A15: 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;

(width (Gauge (C,n))) -' 1 < width (Gauge (C,n)) by A8, A14, NAT_1:14, XREAL_1:233;

then cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) c= UBD C by A1, A11, A15, A12, A7, GOBOARD9:4, JORDAN1A:25;

hence contradiction by A6, A10, JORDAN2C:24, XBOOLE_1:68; :: thesis: verum