let i, n be Element of NAT ; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st i <= len (Gauge (C,n)) holds
cell ((Gauge (C,n)),i,0) c= UBD C
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( i <= len (Gauge (C,n)) implies cell ((Gauge (C,n)),i,0) c= UBD C )
A1: not C ` is empty by JORDAN2C:66;
assume A2: i <= len (Gauge (C,n)) ; :: thesis: cell ((Gauge (C,n)),i,0) c= UBD C
then cell ((Gauge (C,n)),i,0) misses C by JORDAN8:17;
then A3: cell ((Gauge (C,n)),i,0) c= C ` by SUBSET_1:23;
0 <= width (Gauge (C,n)) ;
then ( cell ((Gauge (C,n)),i,0) is connected & not cell ((Gauge (C,n)),i,0) is empty ) by A2, Th45, Th46;
then consider W being Subset of (TOP-REAL 2) such that
A4: W is_a_component_of C ` and
A5: cell ((Gauge (C,n)),i,0) c= W by A3, A1, GOBOARD9:3;
not W is Bounded by A2, A5, Th47, JORDAN2C:12;
then W is_outside_component_of C by A4, JORDAN2C:def 3;
then W c= UBD C by JORDAN2C:23;
hence cell ((Gauge (C,n)),i,0) c= UBD C by A5, XBOOLE_1:1; :: thesis: verum