let i, n be Nat; for E, C being compact non horizontal non vertical Subset of (TOP-REAL 2) st i <= len (Gauge (E,n)) holds
cell ((Gauge (E,n)),i,(width (Gauge (E,n)))) c= UBD E
let E, C be compact non horizontal non vertical Subset of (TOP-REAL 2); ( i <= len (Gauge (E,n)) implies cell ((Gauge (E,n)),i,(width (Gauge (E,n)))) c= UBD E )
assume A1:
i <= len (Gauge (E,n))
; cell ((Gauge (E,n)),i,(width (Gauge (E,n)))) c= UBD E
width (Gauge (E,n)) = len (Gauge (E,n))
by JORDAN8:def 1;
then
cell ((Gauge (E,n)),i,(width (Gauge (E,n)))) misses E
by A1, JORDAN8:15;
then A2:
cell ((Gauge (E,n)),i,(width (Gauge (E,n)))) c= E `
by SUBSET_1:23;
( cell ((Gauge (E,n)),i,(width (Gauge (E,n)))) is connected & not cell ((Gauge (E,n)),i,(width (Gauge (E,n)))) is empty )
by A1, Th24, Th25;
then consider W being Subset of (TOP-REAL 2) such that
A3:
W is_a_component_of E `
and
A4:
cell ((Gauge (E,n)),i,(width (Gauge (E,n)))) c= W
by A2, GOBOARD9:3;
not W is bounded
by A1, A4, Th27, RLTOPSP1:42;
then
W is_outside_component_of E
by A3, JORDAN2C:def 3;
then
W c= UBD E
by JORDAN2C:23;
hence
cell ((Gauge (E,n)),i,(width (Gauge (E,n)))) c= UBD E
by A4; verum