let E be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for j, n being Element of NAT st j <= len (Gauge E,n) holds
cell (Gauge E,n),(len (Gauge E,n)),j c= UBD E
let j, n be Element of NAT ; :: thesis: ( 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:73, JORDAN2C:74;
assume A2: j <= len (Gauge E,n) ; :: thesis: 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:19;
then A3: cell (Gauge E,n),(len (Gauge E,n)),j c= E ` by SUBSET_1:43;
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:45;
cell (Gauge E,n),(len (Gauge E,n)),j is connected by A4, A2, JORDAN1A:46;
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:5;
not W is Bounded by A4, A2, A7, Th37, JORDAN2C:16;
then W is_outside_component_of E by A6, JORDAN2C:def 4;
then W c= UBD E by JORDAN2C:27;
hence cell (Gauge E,n),(len (Gauge E,n)),j c= UBD E by A7, XBOOLE_1:1; :: thesis: verum