let k, n, i, j be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k + 1 <= len (Cage C,n) & [i,j] in Indices (Gauge C,n) & [(i + 1),j] in Indices (Gauge C,n) & (Cage C,n) /. k = (Gauge C,n) * (i + 1),j & (Cage C,n) /. (k + 1) = (Gauge C,n) * i,j holds
j < width (Gauge C,n)
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( 1 <= k & k + 1 <= len (Cage C,n) & [i,j] in Indices (Gauge C,n) & [(i + 1),j] in Indices (Gauge C,n) & (Cage C,n) /. k = (Gauge C,n) * (i + 1),j & (Cage C,n) /. (k + 1) = (Gauge C,n) * i,j implies j < width (Gauge C,n) )
set f = Cage C,n;
set G = Gauge C,n;
assume that
A1: ( 1 <= k & k + 1 <= len (Cage C,n) ) and
A2: [i,j] in Indices (Gauge C,n) and
A3: ( [(i + 1),j] in Indices (Gauge C,n) & (Cage C,n) /. k = (Gauge C,n) * (i + 1),j & (Cage C,n) /. (k + 1) = (Gauge C,n) * i,j ) ; :: thesis: j < width (Gauge C,n)
assume A4: j >= width (Gauge C,n) ; :: thesis: contradiction
j <= width (Gauge C,n) by A2, MATRIX_1:39;
then A5: j = width (Gauge C,n) by A4, XXREAL_0:1;
A6: ( len (Gauge C,n) = width (Gauge C,n) & i <= len (Gauge C,n) ) by A2, JORDAN8:def 1, MATRIX_1:39;
Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
then right_cell (Cage C,n),k,(Gauge C,n) = cell (Gauge C,n),i,j by A1, A2, A3, GOBRD13:27;
hence contradiction by A1, A5, A6, JORDAN8:18, JORDAN9:33; :: thesis: verum