let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for i, n, j being Element of NAT st i <= len (Gauge C,n) & cell (Gauge C,n),i,j c= BDD C holds
j <> width (Gauge C,n)
let i, n, j be Element of 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:71;
assume A4: j = width (Gauge C,n) ; :: thesis: contradiction
not cell (Gauge C,n),i,(width (Gauge C,n)) is empty by A1, JORDAN1A:45;
hence contradiction by A2, A4, A3, JORDAN2C:28, XBOOLE_1:68; :: thesis: verum