let i, j, k, n be Nat; 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,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * ((i + 1),j) holds
j > 1
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ( 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,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * ((i + 1),j) implies j > 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 + 1),j] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * ((i + 1),j) )
; j > 1
assume A4:
j <= 1
; contradiction
1 <= j
by A2, MATRIX_0:32;
then
j = 1
by A4, XXREAL_0:1;
then A5:
j -' 1 = 0
by XREAL_1:232;
A6:
i <= 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,(j -' 1))
by A1, A2, A3, GOBRD13:24;
hence
contradiction
by A1, A5, A6, JORDAN8:17, JORDAN9:31; verum