let E be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: 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; :: 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:66;

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: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; :: thesis: verum

cell ((Gauge (E,n)),(len (Gauge (E,n))),j) c= UBD E

let j, n be 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:66;

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: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; :: thesis: verum