let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for j, n being Element of NAT st j <= width (Gauge C,n) holds
cell (Gauge C,n),0 ,j c= UBD C
let j, n be Element of 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:73, JORDAN2C:74;
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:45;
cell (Gauge C,n),0 ,j misses C by A3, A1, JORDAN8:21;
then A5: cell (Gauge C,n),0 ,j c= C ` by SUBSET_1:43;
cell (Gauge C,n),0 ,j is connected by A3, A1, JORDAN1A:46;
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:5;
not W is Bounded by A1, A7, Th36, JORDAN2C:16;
then W is_outside_component_of C by A6, JORDAN2C:def 4;
then W c= UBD C by JORDAN2C:27;
hence cell (Gauge C,n),0 ,j c= UBD C by A7, XBOOLE_1:1; :: thesis: verum