let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); 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; ( j <= width (Gauge (C,n)) implies cell ((Gauge (C,n)),0,j) c= UBD C )
assume A1:
j <= width (Gauge (C,n))
; 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; verum