let i, n be Element of NAT ; :: thesis: 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); :: thesis: ( 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) ; :: thesis: 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:18;
then A2: cell (Gauge E,n),i,(width (Gauge E,n)) c= E ` by SUBSET_1:43;
A3: not E ` is empty by JORDAN2C:74;
( 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, Th45, Th46;
then consider W being Subset of (TOP-REAL 2) such that
A4: W is_a_component_of E ` and
A5: cell (Gauge E,n),i,(width (Gauge E,n)) c= W by A2, A3, GOBOARD9:5;
not W is Bounded by A1, A5, Th48, JORDAN2C:16;
then W is_outside_component_of E by A4, JORDAN2C:def 4;
then W c= UBD E by JORDAN2C:27;
hence cell (Gauge E,n),i,(width (Gauge E,n)) c= UBD E by A5, XBOOLE_1:1; :: thesis: verum