let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for i, j, n being Nat st i <= len (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
j <> width (Gauge (C,n))
let i, j, n be Nat; :: thesis: ( i <= len (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C implies j <> width (Gauge (C,n)) )
assume that
A1: i <= len (Gauge (C,n)) and
A2: cell ((Gauge (C,n)),i,j) c= BDD C ; :: thesis: j <> width (Gauge (C,n))
A3: cell ((Gauge (C,n)),i,(width (Gauge (C,n)))) c= UBD C by A1, JORDAN1A:50;
assume A4: j = width (Gauge (C,n)) ; :: thesis: contradiction
not cell ((Gauge (C,n)),i,(width (Gauge (C,n)))) is empty by A1, JORDAN1A:24;
hence contradiction by A2, A4, A3, JORDAN2C:24, XBOOLE_1:68; :: thesis: verum