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)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C holds
i > 1
let i, j, n be Nat; :: thesis: ( i <= len (Gauge (C,n)) & j <= width (Gauge (C,n)) & cell ((Gauge (C,n)),i,j) c= BDD C implies i > 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: i <= 1 ; :: thesis: contradiction

per cases ( i = 0 or i = 1 ) by A4, NAT_1:25;

suppose i = 0 ; :: thesis: contradiction

hence contradiction by A2, A3, Lm3; :: thesis: verum

end;

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

BDD C c= C ` by JORDAN2C:25;
then A6: cell ((Gauge (C,n)),1,j) c= C ` by A3, A5;
A7: j <> 0 by A1, A3, Lm4;
UBD C is_outside_component_of C by JORDAN2C:68;
then A8: UBD C is_a_component_of C ` by JORDAN2C:def 3;
A9: len (Gauge (C,n)) <> 0 by MATRIX_0:def 10;
then A10: 0 + 1 <= len (Gauge (C,n)) by NAT_1:14;
then A11: not cell ((Gauge (C,n)),1,j) is empty by A2, JORDAN1A:24;
j < width (Gauge (C,n)) by A1, A2, A3, Lm6, XXREAL_0:1;
then (cell ((Gauge (C,n)),0,j)) /\ (cell ((Gauge (C,n)),(0 + 1),j)) = LSeg (((Gauge (C,n)) * ((0 + 1),j)),((Gauge (C,n)) * ((0 + 1),(j + 1)))) by A9, A7, GOBOARD5:25, NAT_1:14;
then A12: cell ((Gauge (C,n)),0,j) meets cell ((Gauge (C,n)),(0 + 1),j) by XBOOLE_0:def 7;
cell ((Gauge (C,n)),0,j) c= UBD C by A2, Th35;
then cell ((Gauge (C,n)),1,j) c= UBD C by A2, A10, A12, A8, A6, GOBOARD9:4, JORDAN1A:25;
hence contradiction by A3, A5, A11, JORDAN2C:24, XBOOLE_1:68; :: thesis: verum

end;

end;