let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for j, n being Nat st j <= width (Gauge (C,n)) holds

cell ((Gauge (C,n)),0,j) c= UBD C

let j, n be Nat; :: thesis: ( j <= width (Gauge (C,n)) implies cell ((Gauge (C,n)),0,j) c= UBD C )

assume A1: j <= width (Gauge (C,n)) ; :: thesis: cell ((Gauge (C,n)),0,j) c= UBD C

A2: not C ` is empty by JORDAN2C:66;

A3: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;

then A4: not cell ((Gauge (C,n)),0,j) is empty by A1, JORDAN1A:24;

cell ((Gauge (C,n)),0,j) misses C by A3, A1, JORDAN8:18;

then A5: cell ((Gauge (C,n)),0,j) c= C ` by SUBSET_1:23;

cell ((Gauge (C,n)),0,j) is connected by A3, A1, JORDAN1A:25;

then consider W being Subset of (TOP-REAL 2) such that

A6: W is_a_component_of C ` and

A7: cell ((Gauge (C,n)),0,j) c= W by A5, A2, A4, GOBOARD9:3;

not W is bounded by A1, A7, Th33, RLTOPSP1:42;

then W is_outside_component_of C by A6, JORDAN2C:def 3;

then W c= UBD C by JORDAN2C:23;

hence cell ((Gauge (C,n)),0,j) c= UBD C by A7; :: thesis: verum

cell ((Gauge (C,n)),0,j) c= UBD C

let j, n be Nat; :: thesis: ( j <= width (Gauge (C,n)) implies cell ((Gauge (C,n)),0,j) c= UBD C )

assume A1: j <= width (Gauge (C,n)) ; :: thesis: cell ((Gauge (C,n)),0,j) c= UBD C

A2: not C ` is empty by JORDAN2C:66;

A3: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;

then A4: not cell ((Gauge (C,n)),0,j) is empty by A1, JORDAN1A:24;

cell ((Gauge (C,n)),0,j) misses C by A3, A1, JORDAN8:18;

then A5: cell ((Gauge (C,n)),0,j) c= C ` by SUBSET_1:23;

cell ((Gauge (C,n)),0,j) is connected by A3, A1, JORDAN1A:25;

then consider W being Subset of (TOP-REAL 2) such that

A6: W is_a_component_of C ` and

A7: cell ((Gauge (C,n)),0,j) c= W by A5, A2, A4, GOBOARD9:3;

not W is bounded by A1, A7, Th33, RLTOPSP1:42;

then W is_outside_component_of C by A6, JORDAN2C:def 3;

then W c= UBD C by JORDAN2C:23;

hence cell ((Gauge (C,n)),0,j) c= UBD C by A7; :: thesis: verum