let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for i, j, n being Nat st j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds

i <> len (Gauge (C,n))

let i, j, n be Nat; :: thesis: ( j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C implies i <> len (Gauge (C,n)) )

assume that

A1: j <= width (Gauge (C,n)) and

A2: cell ((Gauge (C,n)),i,j) c= BDD C ; :: thesis: i <> len (Gauge (C,n))

A3: not cell ((Gauge (C,n)),(len (Gauge (C,n))),j) is empty by A1, JORDAN1A:24;

assume A4: i = len (Gauge (C,n)) ; :: thesis: contradiction

len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;

then cell ((Gauge (C,n)),(len (Gauge (C,n))),j) c= UBD C by A1, Th36;

hence contradiction by A2, A4, A3, JORDAN2C:24, XBOOLE_1:68; :: thesis: verum

i <> len (Gauge (C,n))

let i, j, n be Nat; :: thesis: ( j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C implies i <> len (Gauge (C,n)) )

assume that

A1: j <= width (Gauge (C,n)) and

A2: cell ((Gauge (C,n)),i,j) c= BDD C ; :: thesis: i <> len (Gauge (C,n))

A3: not cell ((Gauge (C,n)),(len (Gauge (C,n))),j) is empty by A1, JORDAN1A:24;

assume A4: i = len (Gauge (C,n)) ; :: thesis: contradiction

len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;

then cell ((Gauge (C,n)),(len (Gauge (C,n))),j) c= UBD C by A1, Th36;

hence contradiction by A2, A4, A3, JORDAN2C:24, XBOOLE_1:68; :: thesis: verum