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) & j <= width (Gauge C,n) & cell (Gauge C,n),i,j c= BDD C holds
j > 1
let i, n, j be Element of NAT ; :: thesis: ( i <= len (Gauge C,n) & j <= width (Gauge C,n) & cell (Gauge C,n),i,j c= BDD C implies j > 1 )
assume that
A1: i <= len (Gauge C,n) and
A2: j <= width (Gauge C,n) and
A3: cell (Gauge C,n),i,j c= BDD C and
A4: j <= 1 ; :: thesis: contradiction

per cases ( j = 0 or j = 1 ) by A4, NAT_1:26;

suppose j = 0 ; :: thesis: contradiction

hence contradiction by A1, A3, Lm4; :: thesis: verum

end;

suppose A5: j = 1 ; :: thesis: contradiction

BDD C c= C ` by JORDAN2C:29;
then A6: cell (Gauge C,n),i,1 c= C ` by A3, A5, XBOOLE_1:1;
A7: i <> 0 by A2, A3, Lm3;
UBD C is_outside_component_of C by JORDAN2C:73, JORDAN2C:76;
then A8: UBD C is_a_component_of C ` by JORDAN2C:def 4;
A9: width (Gauge C,n) <> 0 by GOBOARD1:def 5;
then A10: 0 + 1 <= width (Gauge C,n) by NAT_1:14;
then A11: not cell (Gauge C,n),i,1 is empty by A1, JORDAN1A:45;
i < len (Gauge C,n) by A1, A2, A3, Lm5, XXREAL_0:1;
then (cell (Gauge C,n),i,0 ) /\ (cell (Gauge C,n),i,(0 + 1)) = LSeg ((Gauge C,n) * i,(0 + 1)),((Gauge C,n) * (i + 1),(0 + 1)) by A9, A7, GOBOARD5:27, NAT_1:14;
then A12: cell (Gauge C,n),i,0 meets cell (Gauge C,n),i,(0 + 1) by XBOOLE_0:def 7;
cell (Gauge C,n),i,0 c= UBD C by A1, JORDAN1A:70;
then cell (Gauge C,n),i,1 c= UBD C by A1, A10, A12, A8, A6, GOBOARD9:6, JORDAN1A:46;
hence contradiction by A3, A5, A11, JORDAN2C:28, XBOOLE_1:68; :: thesis: verum

end;

end;