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