let i, j, k, n be 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_0:32;
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_0:32;
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:26;
hence contradiction by A1, A5, A6, JORDAN8:15, JORDAN9:31; :: thesis: verum