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 <> 0

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

assume that

A1: i <= len (Gauge (C,n)) and

A2: cell ((Gauge (C,n)),i,j) c= BDD C and

A3: j = 0 ; :: thesis: contradiction

A4: cell ((Gauge (C,n)),i,0) c= UBD C by A1, JORDAN1A:49;

0 <= width (Gauge (C,n)) ;

then not cell ((Gauge (C,n)),i,0) is empty by A1, JORDAN1A:24;

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

j <> 0

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

assume that

A1: i <= len (Gauge (C,n)) and

A2: cell ((Gauge (C,n)),i,j) c= BDD C and

A3: j = 0 ; :: thesis: contradiction

A4: cell ((Gauge (C,n)),i,0) c= UBD C by A1, JORDAN1A:49;

0 <= width (Gauge (C,n)) ;

then not cell ((Gauge (C,n)),i,0) is empty by A1, JORDAN1A:24;

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