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 + 1)) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,j) holds
i > 1
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 + 1)) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,j) implies i > 1 )
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 + 1)) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,j) ) ; :: thesis: i > 1
assume A4: i <= 1 ; :: thesis: contradiction
1 <= i by A2, MATRIX_0:32;
then i = 1 by A4, XXREAL_0:1;
then A5: i -' 1 = 0 by XREAL_1:232;
len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
then A6: j <= len (Gauge (C,n)) by A2, 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 -' 1),j) by A1, A2, A3, GOBRD13:28;
hence contradiction by A1, A5, A6, JORDAN8:18, JORDAN9:31; :: thesis: verum