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 <> 0
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 <> 0 )
assume that
A1: j <= width (Gauge (C,n)) and
A2: cell ((Gauge (C,n)),i,j) c= BDD C and
A3: i = 0 ; :: thesis: contradiction
A4: cell ((Gauge (C,n)),0,j) c= UBD C by A1, Th38;
0 <= len (Gauge (C,n)) ;
then not cell ((Gauge (C,n)),0,j) is empty by A1, JORDAN1A:45;
hence contradiction by A2, A3, A4, JORDAN2C:28, XBOOLE_1:68; :: thesis: verum