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

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

j > 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 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:25;

end;

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

BDD C c= C `
by JORDAN2C:25;

then A6: cell ((Gauge (C,n)),i,1) c= C ` by A3, A5;

A7: i <> 0 by A2, A3, Lm3;

UBD C is_outside_component_of C by JORDAN2C:68;

then A8: UBD C is_a_component_of C ` by JORDAN2C:def 3;

A9: width (Gauge (C,n)) <> 0 by MATRIX_0:def 10;

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:24;

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:26, 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:49;

then cell ((Gauge (C,n)),i,1) c= UBD C by A1, A10, A12, A8, A6, GOBOARD9:4, JORDAN1A:25;

hence contradiction by A3, A5, A11, JORDAN2C:24, XBOOLE_1:68; :: thesis: verum

end;then A6: cell ((Gauge (C,n)),i,1) c= C ` by A3, A5;

A7: i <> 0 by A2, A3, Lm3;

UBD C is_outside_component_of C by JORDAN2C:68;

then A8: UBD C is_a_component_of C ` by JORDAN2C:def 3;

A9: width (Gauge (C,n)) <> 0 by MATRIX_0:def 10;

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:24;

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:26, 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:49;

then cell ((Gauge (C,n)),i,1) c= UBD C by A1, A10, A12, A8, A6, GOBOARD9:4, JORDAN1A:25;

hence contradiction by A3, A5, A11, JORDAN2C:24, XBOOLE_1:68; :: thesis: verum