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,(j + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,(j + 1)) holds
i < len (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,(j + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,(j + 1)) implies i < len (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,(j + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,(j + 1)) ) ; :: thesis: i < len (Gauge (C,n))
assume A4: i >= len (Gauge (C,n)) ; :: thesis: contradiction
len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
then A5: j <= len (Gauge (C,n)) by A2, MATRIX_0:32;
i <= len (Gauge (C,n)) by A2, MATRIX_0:32;
then A6: i = len (Gauge (C,n)) by A4, XXREAL_0:1;
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:22;
hence contradiction by A1, A6, A5, JORDAN8:16, JORDAN9:31; :: thesis: verum