let E be compact non horizontal non vertical Subset of (TOP-REAL 2); for j, n being Nat st j <= len (Gauge (E,n)) holds
cell ((Gauge (E,n)),(len (Gauge (E,n))),j) c= UBD E
let j, n be Nat; ( j <= len (Gauge (E,n)) implies cell ((Gauge (E,n)),(len (Gauge (E,n))),j) c= UBD E )
A1:
not E ` is empty
by JORDAN2C:66;
assume A2:
j <= len (Gauge (E,n))
; cell ((Gauge (E,n)),(len (Gauge (E,n))),j) c= UBD E
then
cell ((Gauge (E,n)),(len (Gauge (E,n))),j) misses E
by JORDAN8:16;
then A3:
cell ((Gauge (E,n)),(len (Gauge (E,n))),j) c= E `
by SUBSET_1:23;
A4:
width (Gauge (E,n)) = len (Gauge (E,n))
by JORDAN8:def 1;
then A5:
not cell ((Gauge (E,n)),(len (Gauge (E,n))),j) is empty
by A2, JORDAN1A:24;
cell ((Gauge (E,n)),(len (Gauge (E,n))),j) is connected
by A4, A2, JORDAN1A:25;
then consider W being Subset of (TOP-REAL 2) such that
A6:
W is_a_component_of E `
and
A7:
cell ((Gauge (E,n)),(len (Gauge (E,n))),j) c= W
by A3, A1, A5, GOBOARD9:3;
not W is bounded
by A4, A2, A7, Th34, RLTOPSP1:42;
then
W is_outside_component_of E
by A6, JORDAN2C:def 3;
then
W c= UBD E
by JORDAN2C:23;
hence
cell ((Gauge (E,n)),(len (Gauge (E,n))),j) c= UBD E
by A7; verum