let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( C is connected implies for n, k being Nat st 1 <= k & k + 1 <= len (Cage (C,n)) holds
( left_cell ((Cage (C,n)),k,(Gauge (C,n))) misses C & right_cell ((Cage (C,n)),k,(Gauge (C,n))) meets C ) )
assume A1: C is connected ; :: thesis: for n, k being Nat st 1 <= k & k + 1 <= len (Cage (C,n)) holds
( left_cell ((Cage (C,n)),k,(Gauge (C,n))) misses C & right_cell ((Cage (C,n)),k,(Gauge (C,n))) meets C )
let n be Nat; :: thesis: for k being Nat st 1 <= k & k + 1 <= len (Cage (C,n)) holds
( left_cell ((Cage (C,n)),k,(Gauge (C,n))) misses C & right_cell ((Cage (C,n)),k,(Gauge (C,n))) meets C )
set G = Gauge (C,n);
set f = Cage (C,n);
set W = W-bound C;
set E = E-bound C;
set S = S-bound C;
set N = N-bound C;
A2: Cage (C,n) is_sequence_on Gauge (C,n) by A1, Def1;
defpred S1[ Nat] means for m being Nat st 1 <= m & m + 1 <= len ((Cage (C,n)) | $1) holds
( left_cell (((Cage (C,n)) | $1),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | $1),m,(Gauge (C,n))) meets C );
A3: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
A4: len (Gauge (C,n)) = (2 |^ n) + 3 by JORDAN8:def 1;
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A6: for m being Nat st 1 <= m & m + 1 <= len ((Cage (C,n)) | k) holds
( left_cell (((Cage (C,n)) | k),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | k),m,(Gauge (C,n))) meets C ) ; :: thesis: S1[k + 1]
per cases ( k >= len (Cage (C,n)) or k < len (Cage (C,n)) ) ;
suppose k >= len (Cage (C,n)) ; :: thesis: S1[k + 1]
then ( (Cage (C,n)) | k = Cage (C,n) & (Cage (C,n)) | (k + 1) = Cage (C,n) ) by FINSEQ_1:58, NAT_1:12;
hence S1[k + 1] by A6; :: thesis: verum
end;
suppose A7: k < len (Cage (C,n)) ; :: thesis: S1[k + 1]
then A8: len ((Cage (C,n)) | k) = k by FINSEQ_1:59;
A9: 1 <= len (Gauge (C,n)) by A4, NAT_1:12;
A10: (Cage (C,n)) | k is_sequence_on Gauge (C,n) by A2, GOBOARD1:22;
A11: (Cage (C,n)) | (k + 1) is_sequence_on Gauge (C,n) by A2, GOBOARD1:22;
consider i being Nat such that
A12: 1 <= i and
A13: i + 1 <= len (Gauge (C,n)) and
A14: ( (Cage (C,n)) /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) & (Cage (C,n)) /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) ) and
A15: N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) and
N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) by A1, Def1;
let m be Nat; :: thesis: ( 1 <= m & m + 1 <= len ((Cage (C,n)) | (k + 1)) implies ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) )
assume that
A16: 1 <= m and
A17: m + 1 <= len ((Cage (C,n)) | (k + 1)) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
A18: k + 1 <= len (Cage (C,n)) by A7, NAT_1:13;
then A19: len ((Cage (C,n)) | (k + 1)) = k + 1 by FINSEQ_1:59;
A20: 2 |^ n >= n + 1 by NEWTON:85;
now :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
per cases ( k = 0 or k = 1 or k > 1 ) by NAT_1:25;
suppose A21: k = 0 ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
1 <= m + 1 by NAT_1:12;
then m + 1 = 0 + 1 by A17, A21, XXREAL_0:1;
hence ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) by A16; :: thesis: verum
end;
suppose A22: k = 1 ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
1 + 1 <= m + 1 by A16, XREAL_1:6;
then A23: m + 1 = 1 + 1 by A19, A17, A22, XXREAL_0:1;
(Cage (C,n)) | (k + 1) = <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))))*> by A18, A14, A22, FINSEQ_5:81;
then A24: ( ((Cage (C,n)) | (k + 1)) /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) & ((Cage (C,n)) | (k + 1)) /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) ) by FINSEQ_4:17;
1 <= i + 1 by A12, NAT_1:13;
then A25: [(i + 1),(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A3, A13, A9, MATRIX_0:30;
A26: i < len (Gauge (C,n)) by A13, NAT_1:13;
then A27: [i,(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A3, A12, A9, MATRIX_0:30;
A28: ( i < i + 1 & i + 1 < (i + 1) + 1 ) by NAT_1:13;
then A29: left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i,(len (Gauge (C,n)))) by A3, A11, A17, A24, A27, A25, A23, GOBRD13:def 3;
now :: thesis: not left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
N-bound C > S-bound C by JORDAN8:9;
then (N-bound C) - (S-bound C) > (S-bound C) - (S-bound C) by XREAL_1:9;
then ((N-bound C) - (S-bound C)) / (2 |^ n) > 0 by A20, XREAL_1:139;
then A30: (N-bound C) + 0 < (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n)) by XREAL_1:6;
assume left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ; :: thesis: contradiction
then consider p being object such that
A31: p in cell ((Gauge (C,n)),i,(len (Gauge (C,n)))) and
A32: p in C by A29, XBOOLE_0:3;
reconsider p = p as Element of (TOP-REAL 2) by A31;
A33: p `2 <= N-bound C by A32, PSCOMP_1:24;
[1,(len (Gauge (C,n)))] in Indices (Gauge (C,n)) by A3, A9, MATRIX_0:30;
then (Gauge (C,n)) * (1,(len (Gauge (C,n)))) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge (C,n))) - 2)))]| by JORDAN8:def 1;
then A34: ((Gauge (C,n)) * (1,(len (Gauge (C,n))))) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge (C,n))) - 2)) by EUCLID:52;
cell ((Gauge (C,n)),i,(len (Gauge (C,n)))) = { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (i,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i + 1),1)) `1 & ((Gauge (C,n)) * (1,(len (Gauge (C,n))))) `2 <= s ) } by A3, A12, A26, GOBRD11:31;
then consider r, s being Real such that
A35: p = |[r,s]| and
((Gauge (C,n)) * (i,1)) `1 <= r and
r <= ((Gauge (C,n)) * ((i + 1),1)) `1 and
A36: ((Gauge (C,n)) * (1,(len (Gauge (C,n))))) `2 <= s by A31;
(((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge (C,n))) - 2) = ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (2 |^ n)) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * 1) by A4
.= ((N-bound C) - (S-bound C)) + (((N-bound C) - (S-bound C)) / (2 |^ n)) by A20, XCMPLX_1:87 ;
then N-bound C < s by A36, A34, A30, XXREAL_0:2;
hence contradiction by A35, A33, EUCLID:52; :: thesis: verum
end;
hence left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C ; :: thesis: right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
( N-min C in C & N-min C in right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) ) by A3, A11, A15, A17, A24, A27, A25, A23, A28, GOBRD13:def 2, SPRECT_1:11;
hence right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by XBOOLE_0:3; :: thesis: verum
end;
suppose A37: k > 1 ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
then A38: ((len ((Cage (C,n)) | k)) -' 1) + 1 = len ((Cage (C,n)) | k) by A8, XREAL_1:235;
A39: 1 <= (len ((Cage (C,n)) | k)) -' 1 by A8, A37, NAT_D:49;
now :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
per cases ( m + 1 = len ((Cage (C,n)) | (k + 1)) or m + 1 <> len ((Cage (C,n)) | (k + 1)) ) ;
suppose A40: m + 1 = len ((Cage (C,n)) | (k + 1)) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
A41: len ((Cage (C,n)) | k) <= len (Cage (C,n)) by FINSEQ_5:16;
now :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
left_cell (((Cage (C,n)) | k),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) misses C by A6, A39, A38;
then A42: left_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) misses C by A2, A8, A39, A38, A41, GOBRD13:31;
A43: ((len ((Cage (C,n)) | k)) -' 1) + (1 + 1) = (len ((Cage (C,n)) | k)) + 1 by A38;
right_cell (((Cage (C,n)) | k),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) meets C by A6, A39, A38;
then A44: right_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) meets C by A2, A8, A39, A38, A41, GOBRD13:31;
consider i1, j1, i2, j2 being Nat such that
A45: ( [i1,j1] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) -' 1) = (Gauge (C,n)) * (i1,j1) ) and
A46: [i2,j2] in Indices (Gauge (C,n)) and
A47: (Cage (C,n)) /. (len ((Cage (C,n)) | k)) = (Gauge (C,n)) * (i2,j2) and
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A2, A7, A8, A39, A38, JORDAN8:3;
1 <= i2 by A46, MATRIX_0:32;
then A48: (i2 -' 1) + 1 = i2 by XREAL_1:235;
1 <= j2 by A46, MATRIX_0:32;
then A49: (j2 -' 1) + 1 = j2 by XREAL_1:235;
per cases ( ( front_left_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) misses C ) or ( front_left_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) meets C ) or front_left_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) meets C ) ;
suppose A50: ( front_left_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) misses C ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
then A51: Cage (C,n) turns_right (len ((Cage (C,n)) | k)) -' 1, Gauge (C,n) by A1, A18, A8, A39, A43, Def1;
now :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
per cases ( ( i1 = i2 & j1 + 1 = j2 & [(i2 + 1),j2] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * ((i2 + 1),j2) ) or ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * (i2,(j2 -' 1)) ) or ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * (i2,(j2 + 1)) ) or ( i1 = i2 & j1 = j2 + 1 & [(i2 -' 1),j2] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * ((i2 -' 1),j2) ) ) by A38, A45, A46, A47, A51;
suppose that A52: ( i1 = i2 & j1 + 1 = j2 ) and
A53: ( [(i2 + 1),j2] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * ((i2 + 1),j2) ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
front_right_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j2) by A2, A39, A38, A41, A45, A46, A47, A52, GOBRD13:35;
then left_cell ((Cage (C,n)),m,(Gauge (C,n))) misses C by A2, A18, A8, A19, A16, A40, A46, A47, A50, A52, A53, GOBRD13:23;
hence left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
( j2 -' 1 = j1 & cell ((Gauge (C,n)),i1,j1) meets C ) by A2, A39, A38, A41, A45, A46, A47, A44, A52, GOBRD13:22, NAT_D:34;
then right_cell ((Cage (C,n)),m,(Gauge (C,n))) meets C by A2, A18, A8, A19, A16, A40, A46, A47, A52, A53, GOBRD13:24;
hence right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: verum
end;
suppose that A54: ( i1 + 1 = i2 & j1 = j2 ) and
A55: ( [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * (i2,(j2 -' 1)) ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
front_right_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) by A2, A39, A38, A41, A45, A46, A47, A54, GOBRD13:37;
then left_cell ((Cage (C,n)),m,(Gauge (C,n))) misses C by A2, A18, A8, A19, A16, A40, A46, A47, A49, A50, A55, GOBRD13:27;
hence left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
( i2 -' 1 = i1 & cell ((Gauge (C,n)),i1,(j1 -' 1)) meets C ) by A2, A39, A38, A41, A45, A46, A47, A44, A54, GOBRD13:24, NAT_D:34;
then right_cell ((Cage (C,n)),m,(Gauge (C,n))) meets C by A2, A18, A8, A19, A16, A40, A46, A47, A49, A54, A55, GOBRD13:28;
hence right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: verum
end;
suppose that A56: ( i1 = i2 + 1 & j1 = j2 ) and
A57: ( [i2,(j2 + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * (i2,(j2 + 1)) ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
front_right_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i2 -' 1),j2) by A2, A39, A38, A41, A45, A46, A47, A56, GOBRD13:39;
then left_cell ((Cage (C,n)),m,(Gauge (C,n))) misses C by A2, A18, A8, A19, A16, A40, A46, A47, A50, A57, GOBRD13:21;
hence left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell ((Gauge (C,n)),i2,j2) meets C by A2, A39, A38, A41, A45, A46, A47, A44, A56, GOBRD13:26;
then right_cell ((Cage (C,n)),m,(Gauge (C,n))) meets C by A2, A18, A8, A19, A16, A40, A46, A47, A57, GOBRD13:22;
hence right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: verum
end;
suppose that A58: ( i1 = i2 & j1 = j2 + 1 ) and
A59: ( [(i2 -' 1),j2] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * ((i2 -' 1),j2) ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
front_right_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) by A2, A39, A38, A41, A45, A46, A47, A58, GOBRD13:41;
then left_cell ((Cage (C,n)),m,(Gauge (C,n))) misses C by A2, A18, A8, A19, A16, A40, A46, A47, A48, A50, A59, GOBRD13:25;
hence left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
cell ((Gauge (C,n)),(i2 -' 1),j2) meets C by A2, A39, A38, A41, A45, A46, A47, A44, A58, GOBRD13:28;
then right_cell ((Cage (C,n)),m,(Gauge (C,n))) meets C by A2, A18, A8, A19, A16, A40, A46, A47, A48, A59, GOBRD13:26;
hence right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: verum
end;
end;
end;
hence ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; :: thesis: verum
end;
suppose A60: ( front_left_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) misses C & front_right_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) meets C ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
then A61: Cage (C,n) goes_straight (len ((Cage (C,n)) | k)) -' 1, Gauge (C,n) by A1, A18, A8, A39, A43, Def1;
now :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
per cases ( ( i1 = i2 & j1 + 1 = j2 & [i2,(j2 + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * (i2,(j2 + 1)) ) or ( i1 + 1 = i2 & j1 = j2 & [(i2 + 1),j2] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * ((i2 + 1),j2) ) or ( i1 = i2 + 1 & j1 = j2 & [(i2 -' 1),j2] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * ((i2 -' 1),j2) ) or ( i1 = i2 & j1 = j2 + 1 & [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * (i2,(j2 -' 1)) ) ) by A38, A45, A46, A47, A61;
suppose that A62: ( i1 = i2 & j1 + 1 = j2 ) and
A63: ( [i2,(j2 + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * (i2,(j2 + 1)) ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
front_left_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j2) by A2, A39, A38, A41, A45, A46, A47, A62, GOBRD13:34;
then left_cell ((Cage (C,n)),m,(Gauge (C,n))) misses C by A2, A18, A8, A19, A16, A40, A46, A47, A60, A62, A63, GOBRD13:21;
hence left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
front_right_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j2) by A2, A39, A38, A41, A45, A46, A47, A62, GOBRD13:35;
then right_cell ((Cage (C,n)),m,(Gauge (C,n))) meets C by A2, A18, A8, A19, A16, A40, A46, A47, A60, A62, A63, GOBRD13:22;
hence right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: verum
end;
suppose that A64: ( i1 + 1 = i2 & j1 = j2 ) and
A65: ( [(i2 + 1),j2] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * ((i2 + 1),j2) ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
front_left_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j2) by A2, A39, A38, A41, A45, A46, A47, A64, GOBRD13:36;
then left_cell ((Cage (C,n)),m,(Gauge (C,n))) misses C by A2, A18, A8, A19, A16, A40, A46, A47, A60, A65, GOBRD13:23;
hence left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
front_right_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) by A2, A39, A38, A41, A45, A46, A47, A64, GOBRD13:37;
then right_cell ((Cage (C,n)),m,(Gauge (C,n))) meets C by A2, A18, A8, A19, A16, A40, A46, A47, A60, A65, GOBRD13:24;
hence right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: verum
end;
suppose that A66: ( i1 = i2 + 1 & j1 = j2 ) and
A67: ( [(i2 -' 1),j2] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * ((i2 -' 1),j2) ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
front_left_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) by A2, A39, A38, A41, A45, A46, A47, A66, GOBRD13:38;
then left_cell ((Cage (C,n)),m,(Gauge (C,n))) misses C by A2, A18, A8, A19, A16, A40, A46, A47, A48, A60, A67, GOBRD13:25;
hence left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
front_right_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i2 -' 1),j2) by A2, A39, A38, A41, A45, A46, A47, A66, GOBRD13:39;
then right_cell ((Cage (C,n)),m,(Gauge (C,n))) meets C by A2, A18, A8, A19, A16, A40, A46, A47, A48, A60, A67, GOBRD13:26;
hence right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: verum
end;
suppose that A68: ( i1 = i2 & j1 = j2 + 1 ) and
A69: ( [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * (i2,(j2 -' 1)) ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
front_left_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) by A2, A39, A38, A41, A45, A46, A47, A68, GOBRD13:40;
then left_cell ((Cage (C,n)),m,(Gauge (C,n))) misses C by A2, A18, A8, A19, A16, A40, A46, A47, A49, A60, A69, GOBRD13:27;
hence left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
front_right_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) by A2, A39, A38, A41, A45, A46, A47, A68, GOBRD13:41;
then right_cell ((Cage (C,n)),m,(Gauge (C,n))) meets C by A2, A18, A8, A19, A16, A40, A46, A47, A49, A60, A69, GOBRD13:28;
hence right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: verum
end;
end;
end;
hence ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; :: thesis: verum
end;
suppose A70: front_left_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) meets C ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
then A71: Cage (C,n) turns_left (len ((Cage (C,n)) | k)) -' 1, Gauge (C,n) by A1, A18, A8, A39, A43, Def1;
now :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
per cases ( ( i1 = i2 & j1 + 1 = j2 & [(i2 -' 1),j2] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * ((i2 -' 1),j2) ) or ( i1 + 1 = i2 & j1 = j2 & [i2,(j2 + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * (i2,(j2 + 1)) ) or ( i1 = i2 + 1 & j1 = j2 & [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * (i2,(j2 -' 1)) ) or ( i1 = i2 & j1 = j2 + 1 & [(i2 + 1),j2] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * ((i2 + 1),j2) ) ) by A38, A45, A46, A47, A71;
suppose that A72: ( i1 = i2 & j1 + 1 = j2 ) and
A73: ( [(i2 -' 1),j2] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * ((i2 -' 1),j2) ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
( j2 -' 1 = j1 & cell ((Gauge (C,n)),(i1 -' 1),j1) misses C ) by A2, A39, A38, A41, A45, A46, A47, A42, A72, GOBRD13:21, NAT_D:34;
then left_cell ((Cage (C,n)),m,(Gauge (C,n))) misses C by A2, A18, A8, A19, A16, A40, A46, A47, A48, A72, A73, GOBRD13:25;
hence left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
front_left_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j2) by A2, A39, A38, A41, A45, A46, A47, A72, GOBRD13:34;
then right_cell ((Cage (C,n)),m,(Gauge (C,n))) meets C by A2, A18, A8, A19, A16, A40, A46, A47, A48, A70, A72, A73, GOBRD13:26;
hence right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: verum
end;
suppose that A74: ( i1 + 1 = i2 & j1 = j2 ) and
A75: ( [i2,(j2 + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * (i2,(j2 + 1)) ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
( i2 -' 1 = i1 & cell ((Gauge (C,n)),i1,j1) misses C ) by A2, A39, A38, A41, A45, A46, A47, A42, A74, GOBRD13:23, NAT_D:34;
then left_cell ((Cage (C,n)),m,(Gauge (C,n))) misses C by A2, A18, A8, A19, A16, A40, A46, A47, A74, A75, GOBRD13:21;
hence left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
front_left_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j2) by A2, A39, A38, A41, A45, A46, A47, A74, GOBRD13:36;
then right_cell ((Cage (C,n)),m,(Gauge (C,n))) meets C by A2, A18, A8, A19, A16, A40, A46, A47, A70, A75, GOBRD13:22;
hence right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: verum
end;
suppose that A76: ( i1 = i2 + 1 & j1 = j2 ) and
A77: ( [i2,(j2 -' 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * (i2,(j2 -' 1)) ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell ((Gauge (C,n)),i2,(j2 -' 1)) misses C by A2, A39, A38, A41, A45, A46, A47, A42, A76, GOBRD13:25;
then left_cell ((Cage (C,n)),m,(Gauge (C,n))) misses C by A2, A18, A8, A19, A16, A40, A46, A47, A49, A77, GOBRD13:27;
hence left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
front_left_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),(i2 -' 1),(j2 -' 1)) by A2, A39, A38, A41, A45, A46, A47, A76, GOBRD13:38;
then right_cell ((Cage (C,n)),m,(Gauge (C,n))) meets C by A2, A18, A8, A19, A16, A40, A46, A47, A49, A70, A77, GOBRD13:28;
hence right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: verum
end;
suppose that A78: ( i1 = i2 & j1 = j2 + 1 ) and
A79: ( [(i2 + 1),j2] in Indices (Gauge (C,n)) & (Cage (C,n)) /. ((len ((Cage (C,n)) | k)) + 1) = (Gauge (C,n)) * ((i2 + 1),j2) ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
cell ((Gauge (C,n)),i2,j2) misses C by A2, A39, A38, A41, A45, A46, A47, A42, A78, GOBRD13:27;
then left_cell ((Cage (C,n)),m,(Gauge (C,n))) misses C by A2, A18, A8, A19, A16, A40, A46, A47, A79, GOBRD13:23;
hence left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C
front_left_cell ((Cage (C,n)),((len ((Cage (C,n)) | k)) -' 1),(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) by A2, A39, A38, A41, A45, A46, A47, A78, GOBRD13:40;
then right_cell ((Cage (C,n)),m,(Gauge (C,n))) meets C by A2, A18, A8, A19, A16, A40, A46, A47, A70, A79, GOBRD13:24;
hence right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C by A2, A18, A19, A16, A40, GOBRD13:31; :: thesis: verum
end;
end;
end;
hence ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; :: thesis: verum
end;
end;
end;
hence ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; :: thesis: verum
end;
suppose m + 1 <> len ((Cage (C,n)) | (k + 1)) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
then m + 1 < len ((Cage (C,n)) | (k + 1)) by A17, XXREAL_0:1;
then A80: m + 1 <= len ((Cage (C,n)) | k) by A8, A19, NAT_1:13;
then consider i1, j1, i2, j2 being Nat such that
A81: [i1,j1] in Indices (Gauge (C,n)) and
A82: ((Cage (C,n)) | k) /. m = (Gauge (C,n)) * (i1,j1) and
A83: [i2,j2] in Indices (Gauge (C,n)) and
A84: ((Cage (C,n)) | k) /. (m + 1) = (Gauge (C,n)) * (i2,j2) and
A85: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10, A16, JORDAN8:3;
A86: ( left_cell (((Cage (C,n)) | k),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | k),m,(Gauge (C,n))) meets C ) by A6, A16, A80;
A87: (Cage (C,n)) | (k + 1) = ((Cage (C,n)) | k) ^ <*((Cage (C,n)) /. (k + 1))*> by A18, FINSEQ_5:82;
1 <= m + 1 by NAT_1:12;
then m + 1 in dom ((Cage (C,n)) | k) by A80, FINSEQ_3:25;
then A88: ((Cage (C,n)) | (k + 1)) /. (m + 1) = (Gauge (C,n)) * (i2,j2) by A84, A87, FINSEQ_4:68;
m <= len ((Cage (C,n)) | k) by A80, NAT_1:13;
then m in dom ((Cage (C,n)) | k) by A16, FINSEQ_3:25;
then A89: ((Cage (C,n)) | (k + 1)) /. m = (Gauge (C,n)) * (i1,j1) by A82, A87, FINSEQ_4:68;
now :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
per cases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A85;
suppose A90: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
then ( left_cell (((Cage (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j1) & right_cell (((Cage (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j1) ) by A10, A16, A80, A81, A82, A83, A84, GOBRD13:21, GOBRD13:22;
hence ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) by A11, A16, A17, A81, A83, A86, A89, A88, A90, GOBRD13:21, GOBRD13:22; :: thesis: verum
end;
suppose A91: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
then ( left_cell (((Cage (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,j1) & right_cell (((Cage (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i1,(j1 -' 1)) ) by A10, A16, A80, A81, A82, A83, A84, GOBRD13:23, GOBRD13:24;
hence ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) by A11, A16, A17, A81, A83, A86, A89, A88, A91, GOBRD13:23, GOBRD13:24; :: thesis: verum
end;
suppose A92: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
then ( left_cell (((Cage (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,(j2 -' 1)) & right_cell (((Cage (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j2) ) by A10, A16, A80, A81, A82, A83, A84, GOBRD13:25, GOBRD13:26;
hence ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) by A11, A16, A17, A81, A83, A86, A89, A88, A92, GOBRD13:25, GOBRD13:26; :: thesis: verum
end;
suppose A93: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C )
then ( left_cell (((Cage (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),i2,j2) & right_cell (((Cage (C,n)) | k),m,(Gauge (C,n))) = cell ((Gauge (C,n)),(i1 -' 1),j2) ) by A10, A16, A80, A81, A82, A83, A84, GOBRD13:27, GOBRD13:28;
hence ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) by A11, A16, A17, A81, A83, A86, A89, A88, A93, GOBRD13:27, GOBRD13:28; :: thesis: verum
end;
end;
end;
hence ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; :: thesis: verum
end;
end;
end;
hence ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; :: thesis: verum
end;
end;
end;
hence ( left_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) misses C & right_cell (((Cage (C,n)) | (k + 1)),m,(Gauge (C,n))) meets C ) ; :: thesis: verum
end;
end;
end;
A94: (Cage (C,n)) | (len (Cage (C,n))) = Cage (C,n) by FINSEQ_1:58;
A95: S1[ 0 ] by CARD_1:27;
for k being Nat holds S1[k] from NAT_1:sch 2(A95, A5);
 hence for k being Nat st 1 <= k & k + 1 <= len (Cage (C,n)) holds
( left_cell ((Cage (C,n)),k,(Gauge (C,n))) misses C & right_cell ((Cage (C,n)),k,(Gauge (C,n))) meets C ) by A94; :: thesis: verum