let f be non constant standard special_circular_sequence; :: thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds
Int (left_cell (f,k)) c= LeftComp f
defpred S₁[ Element of NAT ] means ( 1 <= $1 & $1 + 1 <= len f implies Int (left_cell (f,$1)) c= LeftComp f );
A1: S₁[ 0 ] ;

A2: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

assume that
A4: 1 <= k + 1 and
A5: (k + 1) + 1 <= len f ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

per cases ( k = 0 or k >= 1 ) by NAT_1:14;

suppose k = 0 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

hence Int (left_cell (f,(k + 1))) c= LeftComp f by Def1; :: thesis: verum

end;

suppose A6: k >= 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A7: k + 1 <= len f by A5, NAT_1:13;
A8: k <= k + 1 by NAT_1:11;
then k <= len f by A7, XXREAL_0:2;
then A9: k in dom f by A6, FINSEQ_3:25;
then consider i0, j0 being Element of NAT such that
A10: [i0,j0] in Indices (GoB f) and
A11: f /. k = (GoB f) * (i0,j0) by GOBOARD2:14;
A12: k + 1 in dom f by A4, A7, FINSEQ_3:25;
then consider i1, j1 being Element of NAT such that
A13: [i1,j1] in Indices (GoB f) and
A14: f /. (k + 1) = (GoB f) * (i1,j1) by GOBOARD2:14;
(k + 1) + 1 >= 1 by NAT_1:11;
then A15: (k + 1) + 1 in dom f by A5, FINSEQ_3:25;
then consider i2, j2 being Element of NAT such that
A16: [i2,j2] in Indices (GoB f) and
A17: f /. ((k + 1) + 1) = (GoB f) * (i2,j2) by GOBOARD2:14;
A18: 1 <= i0 by A10, MATRIX_1:38;
A19: i0 <= len (GoB f) by A10, MATRIX_1:38;
A20: 1 <= i1 by A13, MATRIX_1:38;
A21: i1 <= len (GoB f) by A13, MATRIX_1:38;
A22: 1 <= i2 by A16, MATRIX_1:38;
A23: i2 <= len (GoB f) by A16, MATRIX_1:38;
A24: 1 <= j0 by A10, MATRIX_1:38;
A25: j0 <= width (GoB f) by A10, MATRIX_1:38;
A26: 1 <= j1 by A13, MATRIX_1:38;
A27: j1 <= width (GoB f) by A13, MATRIX_1:38;
A28: 1 <= j2 by A16, MATRIX_1:38;
A29: j2 <= width (GoB f) by A16, MATRIX_1:38;
A30: ( i0 = i1 or j0 = j1 ) by A9, A10, A11, A12, A13, A14, GOBOARD2:11;
A31: ( i1 = i2 or j1 = j2 ) by A12, A13, A14, A15, A16, A17, GOBOARD2:11;
reconsider i19 = i1, i09 = i0, i29 = i2, j19 = j1, j09 = j0, j29 = j2 as Element of REAL ;
A32: f is_sequence_on GoB f by GOBOARD5:def 5;
then (abs (i0 - i1)) + (abs (j0 - j1)) = 1 by A9, A10, A11, A12, A13, A14, GOBOARD1:def 9;
then A33: ( ( abs (i09 - i19) = 1 & j0 = j1 ) or ( abs (j09 - j19) = 1 & i0 = i1 ) ) by SEQM_3:42;
then A34: ( i0 = i1 or i0 = i1 + 1 or i0 + 1 = i1 ) by SEQM_3:41;
(abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A12, A13, A14, A15, A16, A17, A32, GOBOARD1:def 9;
then A35: ( ( abs (i19 - i29) = 1 & j1 = j2 ) or ( abs (j19 - j29) = 1 & i1 = i2 ) ) by SEQM_3:42;
then A36: ( i1 = i2 or i1 = i2 + 1 or i1 + 1 = i2 ) by SEQM_3:41;
A37: ( j0 = j1 or j0 = j1 + 1 or j0 + 1 = j1 ) by A33, SEQM_3:41;
A38: ( j1 = j2 or j1 = j2 + 1 or j1 + 1 = j2 ) by A35, SEQM_3:41;

A39: now

assume that
A40: i0 = i2 and
A41: j0 = j2 ; :: thesis: contradiction

A42: now

assume k <= 1 ; :: thesis: not (k + 1) + 1 >= len f
then A43: k = 1 by A6, XXREAL_0:1;
assume (k + 1) + 1 >= len f ; :: thesis: contradiction
then (k + 1) + 1 = len f by A5, XXREAL_0:1;
hence contradiction by A43, GOBOARD7:34; :: thesis: verum

end;

A44: k < (k + 1) + 1 by A8, NAT_1:13;

per cases ( k > 1 or (k + 1) + 1 < len f ) by A42;

suppose k > 1 ; :: thesis: contradiction

hence contradiction by A5, A11, A17, A40, A41, A44, GOBOARD7:37; :: thesis: verum

end;

suppose (k + 1) + 1 < len f ; :: thesis: contradiction

hence contradiction by A6, A11, A17, A40, A41, A44, GOBOARD7:36; :: thesis: verum

end;

end;

end;

i1 >= 1 by A13, MATRIX_1:38;
then A45: i1 = (i1 -' 1) + 1 by XREAL_1:235;
j1 >= 1 by A13, MATRIX_1:38;
then A46: j1 = (j1 -' 1) + 1 by XREAL_1:235;
then j1 -' 1 <= j1 by NAT_1:11;
then A47: j1 -' 1 <= width (GoB f) by A27, XXREAL_0:2;
len (GoB f) > 1 by GOBOARD7:32;
then A48: ((len (GoB f)) -' 1) + 1 = len (GoB f) by XREAL_1:235;
width (GoB f) >= 1 by GOBOARD7:33;
then A49: ((width (GoB f)) -' 1) + 1 = width (GoB f) by XREAL_1:235;
A50: (k + 1) + 1 = k + (1 + 1) ;
A51: (i0 + 1) + 1 = i0 + (1 + 1) ;
A52: (i2 + 1) + 1 = i2 + (1 + 1) ;
A53: (j0 + 1) + 1 = j0 + (1 + 1) ;
A54: (j2 + 1) + 1 = j2 + (1 + 1) ;
A55: LeftComp f is_a_component_of (L~ f) ` by Def1;
A56: 0 + 1 = 1 ;

now

per cases ( ( i0 = i1 + 1 & i1 = i2 + 1 & j0 = 1 ) or ( i0 = i1 + 1 & i1 = i2 + 1 & j0 <> 1 ) or ( i0 = i1 + 1 & j1 = j2 + 1 ) or ( j0 = j1 + 1 & i1 = i2 + 1 & i0 = len (GoB f) & j1 = 1 ) or ( j0 = j1 + 1 & i1 = i2 + 1 & i0 <> len (GoB f) & j1 = 1 ) or ( j0 = j1 + 1 & i1 = i2 + 1 & i0 = len (GoB f) & j1 <> 1 ) or ( j0 = j1 + 1 & i1 = i2 + 1 & i0 <> len (GoB f) & j1 <> 1 ) or ( j0 = j1 + 1 & j1 = j2 + 1 & i0 = len (GoB f) ) or ( j0 = j1 + 1 & j1 = j2 + 1 & i0 <> len (GoB f) ) or ( i0 + 1 = i1 & j1 = j2 + 1 & i1 = len (GoB f) & j0 = width (GoB f) ) or ( i0 + 1 = i1 & j1 = j2 + 1 & i1 <> len (GoB f) & j0 = width (GoB f) ) or ( i0 + 1 = i1 & j1 = j2 + 1 & i1 = len (GoB f) & j0 <> width (GoB f) ) or ( i0 + 1 = i1 & j1 = j2 + 1 & i1 <> len (GoB f) & j0 <> width (GoB f) ) or ( j0 + 1 = j1 & i1 = i2 + 1 ) or ( i0 = i1 + 1 & j1 + 1 = j2 & i1 = 1 & j1 = 1 ) or ( i0 = i1 + 1 & j1 + 1 = j2 & i1 <> 1 & j1 = 1 ) or ( i0 = i1 + 1 & j1 + 1 = j2 & i1 = 1 & j1 <> 1 ) or ( i0 = i1 + 1 & j1 + 1 = j2 & i1 <> 1 & j1 <> 1 ) or ( j0 = j1 + 1 & i1 + 1 = i2 ) or ( i0 + 1 = i1 & i1 + 1 = i2 & j0 = width (GoB f) ) or ( i0 + 1 = i1 & i1 + 1 = i2 & j0 <> width (GoB f) ) or ( i0 + 1 = i1 & j1 + 1 = j2 ) or ( j0 + 1 = j1 & i1 + 1 = i2 & i0 = 1 & j1 = width (GoB f) ) or ( j0 + 1 = j1 & i1 + 1 = i2 & i0 <> 1 & j1 = width (GoB f) ) or ( j0 + 1 = j1 & i1 + 1 = i2 & i0 = 1 & j1 <> width (GoB f) ) or ( j0 + 1 = j1 & i1 + 1 = i2 & i0 <> 1 & j1 <> width (GoB f) ) or ( j0 + 1 = j1 & j1 + 1 = j2 & i0 = 1 ) or ( j0 + 1 = j1 & j1 + 1 = j2 & i0 <> 1 ) ) by A9, A11, A12, A14, A15, A17, A34, A36, A37, A38, A39, GOBOARD7:29;

suppose that A57: i0 = i1 + 1 and
A58: i1 = i2 + 1 and
A59: j0 = 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A60: left_cell (f,k) = cell ((GoB f),i1,0) by A6, A7, A10, A11, A13, A14, A30, A56, A57, A59, GOBOARD5:29;
0 + 1 = j2 by A30, A31, A57, A58, A59;
then A61: left_cell (f,(k + 1)) = cell ((GoB f),i2,0) by A4, A5, A13, A14, A16, A17, A30, A57, A58, A59, GOBOARD5:29;
A62: LSeg ((((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * (i1,1)))) - |[0,1]|)) is connected by JORDAN1:6;
A63: LSeg ((((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * (i1,1)))) - |[0,1]|)) meets Int (cell ((GoB f),i1,0)) by A19, A20, A57, GOBOARD6:84;
LSeg ((((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * (i1,1)))) - |[0,1]|)) misses L~ f by A19, A22, A52, A57, A58, GOBOARD8:25;
then LSeg ((((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * (i1,1)))) - |[0,1]|)) c= (L~ f) ` by SUBSET_1:23;
then A64: LSeg ((((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * (i1,1)))) - |[0,1]|)) c= LeftComp f by A3, A5, A6, A55, A60, A62, A63, Th6, NAT_1:13;
A65: LSeg ((((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * (i1,1)))) - |[0,1]|)) meets Int (cell ((GoB f),i2,0)) by A21, A22, A58, GOBOARD6:84;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A61, A64, A65, Th6, Th22; :: thesis: verum

end;

suppose that A66: i0 = i1 + 1 and
A67: i1 = i2 + 1 and
A68: j0 <> 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A69: left_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) by A6, A7, A10, A11, A13, A14, A30, A46, A66, GOBOARD5:29;
1 < j0 by A24, A68, XXREAL_0:1;
then A70: 1 <= j0 -' 1 by A30, A46, A66, NAT_1:13;
A71: left_cell (f,(k + 1)) = cell ((GoB f),i2,(j1 -' 1)) by A4, A5, A13, A14, A16, A17, A31, A46, A67, GOBOARD5:29;
A72: LSeg (((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j0)))),((1 / 2) * (((GoB f) * (i2,(j0 -' 1))) + ((GoB f) * (i1,j0))))) is connected by JORDAN1:6;
A73: LSeg (((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j0)))),((1 / 2) * (((GoB f) * (i2,(j0 -' 1))) + ((GoB f) * (i1,j0))))) meets Int (cell ((GoB f),i1,(j1 -' 1))) by A19, A20, A27, A30, A46, A66, A70, GOBOARD6:82;
LSeg (((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j0)))),((1 / 2) * (((GoB f) * (i2,(j0 -' 1))) + ((GoB f) * (i1,j0))))) misses L~ f by A5, A6, A11, A14, A17, A19, A22, A25, A30, A31, A46, A50, A52, A66, A67, A70, GOBOARD8:11;
then LSeg (((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j0)))),((1 / 2) * (((GoB f) * (i2,(j0 -' 1))) + ((GoB f) * (i1,j0))))) c= (L~ f) ` by SUBSET_1:23;
then A74: LSeg (((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j0)))),((1 / 2) * (((GoB f) * (i2,(j0 -' 1))) + ((GoB f) * (i1,j0))))) c= LeftComp f by A3, A5, A6, A55, A69, A72, A73, Th6, NAT_1:13;
A75: LSeg (((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j0)))),((1 / 2) * (((GoB f) * (i2,(j0 -' 1))) + ((GoB f) * ((i2 + 1),j0))))) meets Int (cell ((GoB f),i2,(j0 -' 1))) by A21, A22, A25, A30, A46, A66, A67, A70, GOBOARD6:82;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A30, A55, A66, A67, A71, A74, A75, Th6, Th22; :: thesis: verum

end;

suppose that A76: i0 = i1 + 1 and
A77: j1 = j2 + 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

left_cell (f,k) = cell ((GoB f),i1,j2) by A6, A7, A10, A11, A13, A14, A30, A76, A77, GOBOARD5:29
.= left_cell (f,(k + 1)) by A4, A5, A13, A14, A16, A17, A31, A45, A77, GOBOARD5:30 ;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A3, A5, A6, NAT_1:13; :: thesis: verum

end;

suppose that A78: j0 = j1 + 1 and
A79: i1 = i2 + 1 and
A80: i0 = len (GoB f) and
A81: j1 = 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A82: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A45, A78, GOBOARD5:30;
A83: LSeg ((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|)) is connected by JORDAN1:6;
A84: LSeg ((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|)) meets Int (cell ((GoB f),i0,j1)) by A25, A78, A80, A81, GOBOARD6:86;
LSeg ((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|)) misses L~ f by GOBOARD8:35;
then LSeg ((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|)) c= (L~ f) ` by SUBSET_1:23;
then A85: LSeg ((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|)) c= LeftComp f by A3, A5, A6, A55, A82, A83, A84, Th6, NAT_1:13;
A86: LSeg ((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|)) meets Int (cell ((GoB f),i1,0)) by A30, A78, A80, GOBOARD6:90;
Int (cell ((GoB f),i1,0)) misses L~ f by A21, A26, A27, GOBOARD7:12;
then Int (cell ((GoB f),i1,0)) c= (L~ f) ` by SUBSET_1:23;
then A87: Int (cell ((GoB f),i1,0)) c= LeftComp f by A21, A26, A27, A55, A85, A86, Th6, Th21;
A88: left_cell (f,(k + 1)) = cell ((GoB f),i2,0) by A4, A5, A13, A14, A16, A17, A31, A46, A79, A81, GOBOARD5:29;
A89: LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) meets Int (cell ((GoB f),i1,0)) by A30, A78, A80, GOBOARD6:90;
LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) misses L~ f by GOBOARD8:27;
then LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) c= (L~ f) ` by SUBSET_1:23;
then A90: LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) c= LeftComp f by A55, A87, A89, Th6, JORDAN1:6;
A91: LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) meets Int (cell ((GoB f),i2,0)) by A22, A30, A45, A78, A79, A80, GOBOARD6:84;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A88, A90, A91, Th6, Th22; :: thesis: verum

end;

suppose that A92: j0 = j1 + 1 and
A93: i1 = i2 + 1 and
A94: i0 <> len (GoB f) and
A95: j1 = 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A96: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A45, A92, GOBOARD5:30;
len (GoB f) > i0 by A19, A94, XXREAL_0:1;
then A97: len (GoB f) >= i0 + 1 by NAT_1:13;
A98: LSeg ((((1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),2))))) is connected by JORDAN1:6;
A99: LSeg ((((1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),(1 + 1)))))) meets Int (cell ((GoB f),i0,j1)) by A20, A25, A30, A92, A95, A97, GOBOARD6:82;
LSeg ((((1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),2))))) misses L~ f by A5, A6, A11, A14, A17, A22, A30, A31, A50, A52, A92, A93, A95, A97, GOBOARD8:8;
then LSeg ((((1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),2))))) c= (L~ f) ` by SUBSET_1:23;
then A100: LSeg ((((1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),2))))) c= LeftComp f by A3, A5, A6, A55, A96, A98, A99, Th6, NAT_1:13;
A101: LSeg ((((1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),2))))) meets Int (cell ((GoB f),i1,0)) by A20, A30, A92, A97, GOBOARD6:84;
Int (cell ((GoB f),i1,0)) misses L~ f by A21, A26, A27, GOBOARD7:12;
then Int (cell ((GoB f),i1,0)) c= (L~ f) ` by SUBSET_1:23;
then A102: Int (cell ((GoB f),i1,0)) c= LeftComp f by A21, A26, A27, A55, A100, A101, Th6, Th21;
A103: left_cell (f,(k + 1)) = cell ((GoB f),i2,0) by A4, A5, A13, A14, A16, A17, A31, A46, A93, A95, GOBOARD5:29;
A104: LSeg ((((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * ((i2 + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i2 + 1),1)) + ((GoB f) * ((i2 + 2),1)))) - |[0,1]|)) meets Int (cell ((GoB f),i1,0)) by A20, A30, A92, A93, A97, GOBOARD6:84;
LSeg ((((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * ((i2 + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i2 + 1),1)) + ((GoB f) * ((i2 + 2),1)))) - |[0,1]|)) misses L~ f by A22, A30, A92, A93, A97, GOBOARD8:25;
then LSeg ((((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * ((i2 + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i2 + 1),1)) + ((GoB f) * ((i2 + 2),1)))) - |[0,1]|)) c= (L~ f) ` by SUBSET_1:23;
then A105: LSeg ((((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * ((i2 + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i2 + 1),1)) + ((GoB f) * ((i2 + 2),1)))) - |[0,1]|)) c= LeftComp f by A55, A102, A104, Th6, JORDAN1:6;
A106: LSeg ((((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * ((i2 + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i2 + 1),1)) + ((GoB f) * ((i2 + 2),1)))) - |[0,1]|)) meets Int (cell ((GoB f),i2,0)) by A21, A22, A93, GOBOARD6:84;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A103, A105, A106, Th6, Th22; :: thesis: verum

end;

suppose that A107: j0 = j1 + 1 and
A108: i1 = i2 + 1 and
A109: i0 = len (GoB f) and
A110: j1 <> 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A111: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A45, A107, GOBOARD5:30;
1 < j1 by A26, A110, XXREAL_0:1;
then A112: 1 <= j1 -' 1 by A46, NAT_1:13;
A113: j1 + 1 = (j1 -' 1) + (1 + 1) by A46;
A114: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) is connected by JORDAN1:6;
A115: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) meets Int (cell ((GoB f),i0,j1)) by A25, A26, A107, A109, GOBOARD6:86;
LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) misses L~ f by A25, A46, A107, A112, A113, GOBOARD8:34;
then LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) c= (L~ f) ` by SUBSET_1:23;
then A116: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) c= LeftComp f by A3, A5, A6, A55, A111, A114, A115, Th6, NAT_1:13;
j1 > 1 by A26, A110, XXREAL_0:1;
then 1 <= j1 -' 1 by A46, NAT_1:13;
then A117: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) meets Int (cell ((GoB f),i1,(j1 -' 1))) by A27, A30, A46, A107, A109, GOBOARD6:86;
Int (cell ((GoB f),i1,(j1 -' 1))) misses L~ f by A21, A47, GOBOARD7:12;
then Int (cell ((GoB f),i1,(j1 -' 1))) c= (L~ f) ` by SUBSET_1:23;
then A118: Int (cell ((GoB f),i1,(j1 -' 1))) c= LeftComp f by A21, A47, A55, A116, A117, Th6, Th21;
A119: left_cell (f,(k + 1)) = cell ((GoB f),i2,(j1 -' 1)) by A4, A5, A13, A14, A16, A17, A31, A46, A108, GOBOARD5:29;
A120: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * (i1,j1)))) + |[1,0]|)) meets Int (cell ((GoB f),i1,(j1 -' 1))) by A27, A30, A46, A107, A109, A112, GOBOARD6:86;
A121: i1 -' 1 = i2 by A108, NAT_D:34;
then LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * (i1,j1)))) + |[1,0]|)) misses L~ f by A5, A6, A11, A14, A17, A25, A30, A31, A46, A50, A107, A108, A109, A112, A113, GOBOARD8:19;
then LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * (i1,j1)))) + |[1,0]|)) c= (L~ f) ` by SUBSET_1:23;
then A122: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * (i1,j1)))) + |[1,0]|)) c= LeftComp f by A55, A118, A120, Th6, JORDAN1:6;
A123: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * (i1,j1)))) + |[1,0]|)) meets Int (cell ((GoB f),i2,(j1 -' 1))) by A21, A22, A27, A46, A108, A112, A121, GOBOARD6:82;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A119, A122, A123, Th6, Th22; :: thesis: verum

end;

suppose that A124: j0 = j1 + 1 and
A125: i1 = i2 + 1 and
A126: i0 <> len (GoB f) and
A127: j1 <> 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A128: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A45, A124, GOBOARD5:30;
1 < j1 by A26, A127, XXREAL_0:1;
then A129: 1 <= j1 -' 1 by A46, NAT_1:13;
len (GoB f) > i0 by A19, A126, XXREAL_0:1;
then A130: len (GoB f) >= i0 + 1 by NAT_1:13;
A131: j1 + 1 = (j1 -' 1) + (1 + 1) by A46;
A132: LSeg (((1 / 2) * (((GoB f) * (i0,(j1 -' 1))) + ((GoB f) * ((i0 + 1),j1)))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) is connected by JORDAN1:6;
A133: LSeg (((1 / 2) * (((GoB f) * (i0,(j1 -' 1))) + ((GoB f) * ((i0 + 1),j1)))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) meets Int (cell ((GoB f),i0,j1)) by A20, A25, A26, A30, A124, A130, GOBOARD6:82;
LSeg (((1 / 2) * (((GoB f) * (i0,(j1 -' 1))) + ((GoB f) * ((i0 + 1),j1)))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) misses L~ f by A5, A6, A11, A14, A17, A22, A25, A30, A31, A46, A50, A52, A124, A125, A129, A130, A131, GOBOARD8:5;
then LSeg (((1 / 2) * (((GoB f) * (i0,(j1 -' 1))) + ((GoB f) * ((i0 + 1),j1)))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) c= (L~ f) ` by SUBSET_1:23;
then A134: LSeg (((1 / 2) * (((GoB f) * (i0,(j1 -' 1))) + ((GoB f) * ((i0 + 1),j1)))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) c= LeftComp f by A3, A5, A6, A55, A128, A132, A133, Th6, NAT_1:13;
j1 > 1 by A26, A127, XXREAL_0:1;
then 1 <= j1 -' 1 by A46, NAT_1:13;
then A135: LSeg (((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * ((i1 + 1),j1)))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) meets Int (cell ((GoB f),i1,(j1 -' 1))) by A20, A27, A30, A46, A124, A130, GOBOARD6:82;
Int (cell ((GoB f),i1,(j1 -' 1))) misses L~ f by A21, A47, GOBOARD7:12;
then Int (cell ((GoB f),i1,(j1 -' 1))) c= (L~ f) ` by SUBSET_1:23;
then A136: Int (cell ((GoB f),i1,(j1 -' 1))) c= LeftComp f by A21, A30, A47, A55, A124, A134, A135, Th6, Th21;
A137: left_cell (f,(k + 1)) = cell ((GoB f),i2,(j1 -' 1)) by A4, A5, A13, A14, A16, A17, A31, A46, A125, GOBOARD5:29;
A138: LSeg (((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * ((i1 + 1),j1)))),((1 / 2) * (((GoB f) * (i2,(j1 -' 1))) + ((GoB f) * (i1,j1))))) meets Int (cell ((GoB f),i1,(j1 -' 1))) by A20, A27, A30, A46, A124, A129, A130, GOBOARD6:82;
i1 < len (GoB f) by A21, A30, A124, A126, XXREAL_0:1;
then i1 + 1 <= len (GoB f) by NAT_1:13;
then LSeg (((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * ((i1 + 1),j1)))),((1 / 2) * (((GoB f) * (i2,(j1 -' 1))) + ((GoB f) * (i1,j1))))) misses L~ f by A5, A6, A11, A14, A17, A22, A25, A30, A31, A46, A50, A52, A124, A125, A129, A131, GOBOARD8:13;
then LSeg (((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * ((i1 + 1),j1)))),((1 / 2) * (((GoB f) * (i2,(j1 -' 1))) + ((GoB f) * (i1,j1))))) c= (L~ f) ` by SUBSET_1:23;
then A139: LSeg (((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * ((i1 + 1),j1)))),((1 / 2) * (((GoB f) * (i2,(j1 -' 1))) + ((GoB f) * (i1,j1))))) c= LeftComp f by A55, A136, A138, Th6, JORDAN1:6;
A140: LSeg (((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * ((i1 + 1),j1)))),((1 / 2) * (((GoB f) * (i2,(j1 -' 1))) + ((GoB f) * ((i2 + 1),j1))))) meets Int (cell ((GoB f),i2,(j1 -' 1))) by A21, A22, A27, A46, A125, A129, GOBOARD6:82;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A125, A137, A139, A140, Th6, Th22; :: thesis: verum

end;

suppose that A141: j0 = j1 + 1 and
A142: j1 = j2 + 1 and
A143: i0 = len (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A144: left_cell (f,k) = cell ((GoB f),(len (GoB f)),j1) by A6, A7, A10, A11, A13, A14, A30, A48, A141, A143, GOBOARD5:30;
A145: left_cell (f,(k + 1)) = cell ((GoB f),(len (GoB f)),j2) by A4, A5, A13, A14, A16, A17, A30, A31, A48, A141, A142, A143, GOBOARD5:30;
A146: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2))))) + |[1,0]|)) is connected by JORDAN1:6;
A147: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2))))) + |[1,0]|)) meets Int (cell ((GoB f),(len (GoB f)),j1)) by A25, A26, A141, A142, GOBOARD6:86;
LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2))))) + |[1,0]|)) misses L~ f by A25, A28, A141, A142, GOBOARD8:34;
then LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2))))) + |[1,0]|)) c= (L~ f) ` by SUBSET_1:23;
then A148: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2))))) + |[1,0]|)) c= LeftComp f by A3, A5, A6, A55, A144, A146, A147, Th6, NAT_1:13;
A149: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2))))) + |[1,0]|)) meets Int (cell ((GoB f),i1,j2)) by A27, A28, A30, A141, A142, A143, GOBOARD6:86;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A30, A55, A141, A143, A145, A148, A149, Th6, Th22; :: thesis: verum

end;

suppose that A150: j0 = j1 + 1 and
A151: j1 = j2 + 1 and
A152: i0 <> len (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A153: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A45, A150, GOBOARD5:30;
len (GoB f) > i0 by A19, A152, XXREAL_0:1;
then A154: len (GoB f) >= i0 + 1 by NAT_1:13;
A155: left_cell (f,(k + 1)) = cell ((GoB f),i1,j2) by A4, A5, A13, A14, A16, A17, A31, A45, A151, GOBOARD5:30;
A156: LSeg (((1 / 2) * (((GoB f) * (i0,j2)) + ((GoB f) * ((i0 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * (i1,(j2 + 1))) + ((GoB f) * ((i1 + 1),(j2 + 2)))))) is connected by JORDAN1:6;
A157: LSeg (((1 / 2) * (((GoB f) * (i0,j2)) + ((GoB f) * ((i0 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * (i1,(j2 + 1))) + ((GoB f) * ((i1 + 1),(j2 + 2)))))) meets Int (cell ((GoB f),i0,j1)) by A20, A25, A26, A30, A150, A151, A154, GOBOARD6:82;
LSeg (((1 / 2) * (((GoB f) * (i0,j2)) + ((GoB f) * ((i0 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * (i1,(j2 + 1))) + ((GoB f) * ((i1 + 1),(j2 + 2)))))) misses L~ f by A5, A6, A11, A14, A17, A18, A25, A28, A30, A31, A50, A150, A151, A154, GOBOARD8:4;
then LSeg (((1 / 2) * (((GoB f) * (i0,j2)) + ((GoB f) * ((i0 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * (i1,(j2 + 1))) + ((GoB f) * ((i1 + 1),(j2 + 2)))))) c= (L~ f) ` by SUBSET_1:23;
then A158: LSeg (((1 / 2) * (((GoB f) * (i0,j2)) + ((GoB f) * ((i0 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * (i1,(j2 + 1))) + ((GoB f) * ((i1 + 1),(j2 + 2)))))) c= LeftComp f by A3, A5, A6, A55, A153, A156, A157, Th6, NAT_1:13;
A159: LSeg (((1 / 2) * (((GoB f) * (i0,j2)) + ((GoB f) * ((i0 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * (i1,(j2 + 1))) + ((GoB f) * ((i1 + 1),(j2 + 2)))))) meets Int (cell ((GoB f),i1,j2)) by A20, A27, A28, A30, A150, A151, A154, GOBOARD6:82;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A155, A158, A159, Th6, Th22; :: thesis: verum

end;

suppose that A160: i0 + 1 = i1 and
A161: j1 = j2 + 1 and
A162: i1 = len (GoB f) and
A163: j0 = width (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A164: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A46, A160, GOBOARD5:28;
A165: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0)))) + |[0,1]|),(((GoB f) * (i1,j0)) + |[1,1]|)) is connected by JORDAN1:6;
A166: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0)))) + |[0,1]|),(((GoB f) * (i1,j0)) + |[1,1]|)) meets Int (cell ((GoB f),i0,j1)) by A18, A21, A30, A160, A163, GOBOARD6:83;
LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0)))) + |[0,1]|),(((GoB f) * (i1,j0)) + |[1,1]|)) misses L~ f by A48, A160, A162, A163, GOBOARD8:30;
then LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0)))) + |[0,1]|),(((GoB f) * (i1,j0)) + |[1,1]|)) c= (L~ f) ` by SUBSET_1:23;
then A167: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0)))) + |[0,1]|),(((GoB f) * (i1,j0)) + |[1,1]|)) c= LeftComp f by A3, A5, A6, A55, A164, A165, A166, Th6, NAT_1:13;
A168: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0)))) + |[0,1]|),(((GoB f) * (i1,j0)) + |[1,1]|)) meets Int (cell ((GoB f),i1,j1)) by A30, A160, A162, A163, GOBOARD6:88;
Int (cell ((GoB f),i1,j1)) misses L~ f by A21, A27, GOBOARD7:12;
then Int (cell ((GoB f),i1,j1)) c= (L~ f) ` by SUBSET_1:23;
then A169: Int (cell ((GoB f),i1,j1)) c= LeftComp f by A21, A27, A55, A167, A168, Th6, Th21;
A170: left_cell (f,(k + 1)) = cell ((GoB f),i1,j2) by A4, A5, A13, A14, A16, A17, A31, A45, A161, GOBOARD5:30;
A171: LSeg ((((1 / 2) * (((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1)))) + |[1,0]|),(((GoB f) * (i1,j1)) + |[1,1]|)) meets Int (cell ((GoB f),i1,j1)) by A30, A160, A162, A163, GOBOARD6:88;
LSeg ((((1 / 2) * (((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1)))) + |[1,0]|),(((GoB f) * (i1,j1)) + |[1,1]|)) misses L~ f by A30, A49, A160, A161, A162, A163, GOBOARD8:36;
then LSeg ((((1 / 2) * (((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1)))) + |[1,0]|),(((GoB f) * (i1,j1)) + |[1,1]|)) c= (L~ f) ` by SUBSET_1:23;
then A172: LSeg ((((1 / 2) * (((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1)))) + |[1,0]|),(((GoB f) * (i1,j1)) + |[1,1]|)) c= LeftComp f by A55, A169, A171, Th6, JORDAN1:6;
A173: LSeg ((((1 / 2) * (((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1)))) + |[1,0]|),(((GoB f) * (i1,j1)) + |[1,1]|)) meets Int (cell ((GoB f),i1,j2)) by A27, A28, A161, A162, GOBOARD6:86;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A170, A172, A173, Th6, Th22; :: thesis: verum

end;

suppose that A174: i0 + 1 = i1 and
A175: j1 = j2 + 1 and
A176: i1 <> len (GoB f) and
A177: j0 = width (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A178: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A46, A174, GOBOARD5:28;
len (GoB f) > i1 by A21, A176, XXREAL_0:1;
then A179: i1 + 1 <= len (GoB f) by NAT_1:13;
A180: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0)))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0)))) + |[0,1]|)) is connected by JORDAN1:6;
A181: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0)))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0)))) + |[0,1]|)) meets Int (cell ((GoB f),i0,j1)) by A18, A21, A30, A174, A177, GOBOARD6:83;
LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0)))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0)))) + |[0,1]|)) misses L~ f by A18, A174, A177, A179, GOBOARD8:28;
then LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0)))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0)))) + |[0,1]|)) c= (L~ f) ` by SUBSET_1:23;
then A182: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0)))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0)))) + |[0,1]|)) c= LeftComp f by A3, A5, A6, A55, A178, A180, A181, Th6, NAT_1:13;
A183: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0)))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0)))) + |[0,1]|)) meets Int (cell ((GoB f),i1,j1)) by A20, A30, A174, A177, A179, GOBOARD6:83;
Int (cell ((GoB f),i1,j1)) misses L~ f by A21, A27, GOBOARD7:12;
then Int (cell ((GoB f),i1,j1)) c= (L~ f) ` by SUBSET_1:23;
then A184: Int (cell ((GoB f),i1,j1)) c= LeftComp f by A21, A27, A55, A182, A183, Th6, Th21;
A185: left_cell (f,(k + 1)) = cell ((GoB f),i1,j2) by A4, A5, A13, A14, A16, A17, A31, A45, A175, GOBOARD5:30;
A186: LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),j0)))),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i1 + 1),j0)))) + |[0,1]|)) meets Int (cell ((GoB f),i1,j1)) by A20, A30, A174, A177, A179, GOBOARD6:83;
LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),j0)))),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i1 + 1),j0)))) + |[0,1]|)) misses L~ f by A5, A6, A11, A14, A17, A18, A30, A31, A49, A50, A51, A174, A175, A177, A179, GOBOARD8:10;
then LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),j0)))),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i1 + 1),j0)))) + |[0,1]|)) c= (L~ f) ` by SUBSET_1:23;
then A187: LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),j0)))),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i1 + 1),j0)))) + |[0,1]|)) c= LeftComp f by A55, A184, A186, Th6, JORDAN1:6;
A188: LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),j0)))),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i1 + 1),j0)))) + |[0,1]|)) meets Int (cell ((GoB f),i1,j2)) by A20, A28, A30, A174, A175, A177, A179, GOBOARD6:82;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A185, A187, A188, Th6, Th22; :: thesis: verum

end;

suppose that A189: i0 + 1 = i1 and
A190: j1 = j2 + 1 and
A191: i1 = len (GoB f) and
A192: j0 <> width (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A193: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A46, A189, GOBOARD5:28;
width (GoB f) > j0 by A25, A192, XXREAL_0:1;
then A194: width (GoB f) >= j0 + 1 by NAT_1:13;
A195: LSeg (((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i1,(j1 + 1))))),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1))))) + |[1,0]|)) is connected by JORDAN1:6;
A196: LSeg (((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i1,(j1 + 1))))),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1))))) + |[1,0]|)) meets Int (cell ((GoB f),i0,j1)) by A18, A21, A26, A30, A189, A194, GOBOARD6:82;
LSeg (((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i1,(j1 + 1))))),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1))))) + |[1,0]|)) misses L~ f by A5, A6, A11, A14, A17, A28, A30, A31, A48, A50, A54, A189, A190, A191, A194, GOBOARD8:20;
then LSeg (((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i1,(j1 + 1))))),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1))))) + |[1,0]|)) c= (L~ f) ` by SUBSET_1:23;
then A197: LSeg (((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i1,(j1 + 1))))),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1))))) + |[1,0]|)) c= LeftComp f by A3, A5, A6, A55, A193, A195, A196, Th6, NAT_1:13;
A198: LSeg (((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i1,(j1 + 1))))),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1))))) + |[1,0]|)) meets Int (cell ((GoB f),i1,j1)) by A26, A30, A189, A191, A194, GOBOARD6:86;
Int (cell ((GoB f),i1,j1)) misses L~ f by A21, A27, GOBOARD7:12;
then Int (cell ((GoB f),i1,j1)) c= (L~ f) ` by SUBSET_1:23;
then A199: Int (cell ((GoB f),i1,j1)) c= LeftComp f by A21, A27, A55, A197, A198, Th6, Th21;
A200: left_cell (f,(k + 1)) = cell ((GoB f),i1,j2) by A4, A5, A13, A14, A16, A17, A31, A45, A190, GOBOARD5:30;
A201: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) meets Int (cell ((GoB f),i1,j1)) by A26, A30, A189, A191, A194, GOBOARD6:86;
LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) misses L~ f by A28, A30, A54, A189, A190, A194, GOBOARD8:34;
then LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) c= (L~ f) ` by SUBSET_1:23;
then A202: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) c= LeftComp f by A55, A199, A201, Th6, JORDAN1:6;
A203: LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) meets Int (cell ((GoB f),i1,j2)) by A27, A28, A190, A191, GOBOARD6:86;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A200, A202, A203, Th6, Th22; :: thesis: verum

end;

suppose that A204: i0 + 1 = i1 and
A205: j1 = j2 + 1 and
A206: i1 <> len (GoB f) and
A207: j0 <> width (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A208: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A46, A204, GOBOARD5:28;
len (GoB f) > i1 by A21, A206, XXREAL_0:1;
then A209: i1 + 1 <= len (GoB f) by NAT_1:13;
width (GoB f) > j0 by A25, A207, XXREAL_0:1;
then A210: width (GoB f) >= j0 + 1 by NAT_1:13;
A211: LSeg (((1 / 2) * (((GoB f) * (i0,(j2 + 1))) + ((GoB f) * ((i0 + 1),(j1 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) is connected by JORDAN1:6;
A212: LSeg (((1 / 2) * (((GoB f) * (i0,(j2 + 1))) + ((GoB f) * ((i0 + 1),(j1 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) meets Int (cell ((GoB f),i0,j1)) by A18, A21, A26, A30, A204, A205, A210, GOBOARD6:82;
LSeg (((1 / 2) * (((GoB f) * (i0,(j2 + 1))) + ((GoB f) * ((i0 + 1),(j1 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) misses L~ f by A5, A6, A11, A14, A17, A18, A28, A30, A31, A50, A51, A54, A204, A205, A209, A210, GOBOARD8:16;
then LSeg (((1 / 2) * (((GoB f) * (i0,(j2 + 1))) + ((GoB f) * ((i0 + 1),(j1 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) c= (L~ f) ` by SUBSET_1:23;
then A213: LSeg (((1 / 2) * (((GoB f) * (i0,(j2 + 1))) + ((GoB f) * ((i0 + 1),(j1 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) c= LeftComp f by A3, A5, A6, A55, A208, A211, A212, Th6, NAT_1:13;
A214: LSeg (((1 / 2) * (((GoB f) * (i0,(j2 + 1))) + ((GoB f) * ((i0 + 1),(j1 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) meets Int (cell ((GoB f),i1,j1)) by A20, A26, A30, A204, A205, A209, A210, GOBOARD6:82;
Int (cell ((GoB f),i1,j1)) misses L~ f by A21, A27, GOBOARD7:12;
then Int (cell ((GoB f),i1,j1)) c= (L~ f) ` by SUBSET_1:23;
then A215: Int (cell ((GoB f),i1,j1)) c= LeftComp f by A21, A27, A55, A213, A214, Th6, Th21;
A216: left_cell (f,(k + 1)) = cell ((GoB f),i1,j2) by A4, A5, A13, A14, A16, A17, A31, A45, A205, GOBOARD5:30;
A217: LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) meets Int (cell ((GoB f),i1,j1)) by A20, A26, A30, A204, A205, A209, A210, GOBOARD6:82;
LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) misses L~ f by A5, A6, A11, A14, A17, A18, A28, A30, A31, A50, A51, A54, A204, A205, A209, A210, GOBOARD8:6;
then LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) c= (L~ f) ` by SUBSET_1:23;
then A218: LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) c= LeftComp f by A55, A215, A217, Th6, JORDAN1:6;
A219: LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) meets Int (cell ((GoB f),i1,j2)) by A20, A27, A28, A204, A205, A209, GOBOARD6:82;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A216, A218, A219, Th6, Th22; :: thesis: verum

end;

suppose that A220: j0 + 1 = j1 and
A221: i1 = i2 + 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

left_cell (f,k) = cell ((GoB f),i2,j0) by A6, A7, A10, A11, A13, A14, A30, A220, A221, GOBOARD5:27
.= left_cell (f,(k + 1)) by A4, A5, A13, A14, A16, A17, A31, A220, A221, GOBOARD5:29 ;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A3, A5, A6, NAT_1:13; :: thesis: verum

end;

suppose that A222: i0 = i1 + 1 and
A223: j1 + 1 = j2 and
A224: i1 = 1 and
A225: j1 = 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A226: left_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) by A6, A7, A10, A11, A13, A14, A30, A46, A222, GOBOARD5:29;
A227: LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1)))) - |[0,1]|)) is connected by JORDAN1:6;
i1 -' 1 <= i1 by NAT_D:35;
then A228: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2;
A229: j1 -' 1 = 0 by A225, XREAL_1:232;
A230: i1 -' 1 = 0 by A224, XREAL_1:232;
j1 -' 1 <= j1 by NAT_D:35;
then A231: j1 -' 1 <= width (GoB f) by A27, XXREAL_0:2;
A232: LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1)))) - |[0,1]|)) meets Int (cell ((GoB f),i1,(j1 -' 1))) by A19, A20, A222, A225, A229, GOBOARD6:84;
LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1)))) - |[0,1]|)) misses L~ f by A222, A224, A225, GOBOARD8:26;
then LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1)))) - |[0,1]|)) c= (L~ f) ` by SUBSET_1:23;
then A233: LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1)))) - |[0,1]|)) c= LeftComp f by A3, A5, A6, A55, A226, A227, A232, Th6, NAT_1:13;
A234: LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1)))) - |[0,1]|)) meets Int (cell ((GoB f),(i1 -' 1),(j0 -' 1))) by A30, A222, A224, A225, A229, GOBOARD6:87;
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) misses L~ f by A228, A231, GOBOARD7:12;
then Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= (L~ f) ` by SUBSET_1:23;
then A235: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= LeftComp f by A30, A55, A222, A228, A231, A233, A234, Th6, Th21;
A236: left_cell (f,(k + 1)) = cell ((GoB f),(i1 -' 1),j1) by A4, A5, A13, A14, A16, A17, A31, A45, A223, GOBOARD5:27;
A237: LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2)))) - |[1,0]|)) meets Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) by A224, A225, A229, GOBOARD6:87;
LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2)))) - |[1,0]|)) misses L~ f by A223, A224, A225, GOBOARD8:32;
then LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2)))) - |[1,0]|)) c= (L~ f) ` by SUBSET_1:23;
then A238: LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2)))) - |[1,0]|)) c= LeftComp f by A55, A235, A237, Th6, JORDAN1:6;
A239: LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2)))) - |[1,0]|)) meets Int (cell ((GoB f),(i1 -' 1),j1)) by A26, A29, A223, A224, A230, GOBOARD6:85;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A236, A238, A239, Th6, Th22; :: thesis: verum

end;

suppose that A240: i0 = i1 + 1 and
A241: j1 + 1 = j2 and
A242: i1 <> 1 and
A243: j1 = 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A244: left_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) by A6, A7, A10, A11, A13, A14, A30, A46, A240, GOBOARD5:29;
1 < i1 by A20, A242, XXREAL_0:1;
then A245: 1 <= i1 -' 1 by A45, NAT_1:13;
A246: (i1 -' 1) + (1 + 1) = i0 by A45, A240;
A247: LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|)) is connected by JORDAN1:6;
i1 -' 1 <= i1 by NAT_D:35;
then A248: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2;
A249: j1 -' 1 = 0 by A243, XREAL_1:232;
j1 -' 1 <= j1 by NAT_D:35;
then A250: j1 -' 1 <= width (GoB f) by A27, XXREAL_0:2;
A251: LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|)) meets Int (cell ((GoB f),i1,(j1 -' 1))) by A19, A20, A240, A249, GOBOARD6:84;
LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|)) misses L~ f by A19, A45, A245, A246, GOBOARD8:25;
then LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|)) c= (L~ f) ` by SUBSET_1:23;
then A252: LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|)) c= LeftComp f by A3, A5, A6, A55, A244, A247, A251, Th6, NAT_1:13;
A253: LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|)) meets Int (cell ((GoB f),(i1 -' 1),(j0 -' 1))) by A21, A30, A45, A240, A245, A249, GOBOARD6:84;
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) misses L~ f by A248, A250, GOBOARD7:12;
then Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= (L~ f) ` by SUBSET_1:23;
then A254: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= LeftComp f by A30, A55, A240, A248, A250, A252, A253, Th6, Th21;
A255: left_cell (f,(k + 1)) = cell ((GoB f),(i1 -' 1),j1) by A4, A5, A13, A14, A16, A17, A31, A45, A241, GOBOARD5:27;
A256: LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,2))))) meets Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) by A21, A45, A245, A249, GOBOARD6:84;
LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,2))))) misses L~ f by A5, A6, A11, A14, A17, A19, A30, A31, A45, A50, A241, A243, A245, A246, GOBOARD8:7;
then LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,2))))) c= (L~ f) ` by SUBSET_1:23;
then A257: LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,2))))) c= LeftComp f by A55, A254, A256, Th6, JORDAN1:6;
A258: LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,2))))) meets Int (cell ((GoB f),(i1 -' 1),j1)) by A21, A29, A45, A241, A243, A245, GOBOARD6:82;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A255, A257, A258, Th6, Th22; :: thesis: verum

end;

suppose that A259: i0 = i1 + 1 and
A260: j1 + 1 = j2 and
A261: i1 = 1 and
A262: j1 <> 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A263: left_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) by A6, A7, A10, A11, A13, A14, A30, A46, A259, GOBOARD5:29;
1 < j0 by A24, A30, A259, A262, XXREAL_0:1;
then A264: 1 <= j0 -' 1 by A30, A46, A259, NAT_1:13;
A265: (j0 -' 1) + (1 + 1) = j2 by A30, A46, A259, A260;
A266: LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (2,((j1 -' 1) + 1)))))) is connected by JORDAN1:6;
A267: LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (2,((j1 -' 1) + 1)))))) meets Int (cell ((GoB f),i1,(j1 -' 1))) by A19, A27, A30, A46, A259, A261, A264, GOBOARD6:82;
LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (2,((j1 -' 1) + 1)))))) misses L~ f by A5, A6, A11, A14, A17, A29, A30, A31, A46, A50, A259, A260, A261, A264, A265, GOBOARD8:17;
then LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (2,((j1 -' 1) + 1)))))) c= (L~ f) ` by SUBSET_1:23;
then A268: LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (2,((j1 -' 1) + 1)))))) c= LeftComp f by A3, A5, A6, A55, A263, A266, A267, Th6, NAT_1:13;
i1 -' 1 <= i1 by NAT_D:35;
then A269: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2;
A270: i1 -' 1 = 0 by A261, XREAL_1:232;
j1 -' 1 <= j1 by NAT_D:35;
then A271: j1 -' 1 <= width (GoB f) by A27, XXREAL_0:2;
A272: LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (2,((j1 -' 1) + 1)))))) meets Int (cell ((GoB f),(i1 -' 1),(j0 -' 1))) by A27, A30, A46, A259, A264, A270, GOBOARD6:85;
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) misses L~ f by A269, A271, GOBOARD7:12;
then Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= (L~ f) ` by SUBSET_1:23;
then A273: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= LeftComp f by A30, A55, A259, A268, A269, A271, A272, Th6, Th21;
A274: left_cell (f,(k + 1)) = cell ((GoB f),(i1 -' 1),j1) by A4, A5, A13, A14, A16, A17, A31, A45, A260, GOBOARD5:27;
A275: LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,((j1 -' 1) + 1))) + ((GoB f) * (1,((j1 -' 1) + 2))))) - |[1,0]|)) meets Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) by A27, A30, A46, A259, A264, A270, GOBOARD6:85;
LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,((j1 -' 1) + 1))) + ((GoB f) * (1,((j1 -' 1) + 2))))) - |[1,0]|)) misses L~ f by A29, A30, A46, A259, A260, A264, GOBOARD8:31;
then LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,((j1 -' 1) + 1))) + ((GoB f) * (1,((j1 -' 1) + 2))))) - |[1,0]|)) c= (L~ f) ` by SUBSET_1:23;
then A276: LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,((j1 -' 1) + 1))) + ((GoB f) * (1,((j1 -' 1) + 2))))) - |[1,0]|)) c= LeftComp f by A55, A273, A275, Th6, JORDAN1:6;
A277: LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,((j1 -' 1) + 1))) + ((GoB f) * (1,((j1 -' 1) + 2))))) - |[1,0]|)) meets Int (cell ((GoB f),(i1 -' 1),j1)) by A26, A29, A46, A260, A270, GOBOARD6:85;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A274, A276, A277, Th6, Th22; :: thesis: verum

end;

suppose that A278: i0 = i1 + 1 and
A279: j1 + 1 = j2 and
A280: i1 <> 1 and
A281: j1 <> 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A282: left_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) by A6, A7, A10, A11, A13, A14, A30, A46, A278, GOBOARD5:29;
1 < j0 by A24, A30, A278, A281, XXREAL_0:1;
then A283: 1 <= j0 -' 1 by A30, A46, A278, NAT_1:13;
1 < i1 by A20, A280, XXREAL_0:1;
then A284: 1 <= i1 -' 1 by A45, NAT_1:13;
A285: (i1 -' 1) + (1 + 1) = i0 by A45, A278;
A286: (j0 -' 1) + (1 + 1) = j2 by A30, A46, A278, A279;
A287: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j0 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j1))))) is connected by JORDAN1:6;
A288: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j0 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j1))))) meets Int (cell ((GoB f),i1,(j1 -' 1))) by A19, A20, A27, A30, A46, A278, A283, GOBOARD6:82;
LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j0 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j1))))) misses L~ f by A5, A6, A11, A14, A17, A19, A29, A30, A31, A45, A46, A50, A279, A283, A284, A285, A286, GOBOARD8:12;
then LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j0 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j1))))) c= (L~ f) ` by SUBSET_1:23;
then A289: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j0 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j1))))) c= LeftComp f by A3, A5, A6, A55, A282, A287, A288, Th6, NAT_1:13;
i1 -' 1 <= i1 by NAT_D:35;
then A290: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2;
j1 -' 1 <= j1 by NAT_D:35;
then A291: j1 -' 1 <= width (GoB f) by A27, XXREAL_0:2;
A292: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j0 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j1))))) meets Int (cell ((GoB f),(i1 -' 1),(j0 -' 1))) by A21, A27, A30, A45, A46, A278, A283, A284, GOBOARD6:82;
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) misses L~ f by A290, A291, GOBOARD7:12;
then Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= (L~ f) ` by SUBSET_1:23;
then A293: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= LeftComp f by A30, A55, A278, A289, A290, A291, A292, Th6, Th21;
A294: left_cell (f,(k + 1)) = cell ((GoB f),(i1 -' 1),j1) by A4, A5, A13, A14, A16, A17, A31, A45, A279, GOBOARD5:27;
A295: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j2))))) meets Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) by A21, A27, A30, A45, A46, A278, A283, A284, GOBOARD6:82;
LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j2))))) misses L~ f by A5, A6, A11, A14, A17, A19, A29, A30, A31, A45, A46, A50, A279, A283, A284, A285, A286, GOBOARD8:2;
then LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j2))))) c= (L~ f) ` by SUBSET_1:23;
then A296: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j2))))) c= LeftComp f by A55, A293, A295, Th6, JORDAN1:6;
A297: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j2))))) meets Int (cell ((GoB f),(i1 -' 1),j1)) by A21, A26, A29, A45, A279, A284, GOBOARD6:82;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A294, A296, A297, Th6, Th22; :: thesis: verum

end;

suppose that A298: j0 = j1 + 1 and
A299: i1 + 1 = i2 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A45, A298, GOBOARD5:30
.= left_cell (f,(k + 1)) by A4, A5, A13, A14, A16, A17, A30, A31, A46, A298, A299, GOBOARD5:28 ;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A3, A5, A6, NAT_1:13; :: thesis: verum

end;

suppose that A300: i0 + 1 = i1 and
A301: i1 + 1 = i2 and
A302: j0 = width (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A303: left_cell (f,k) = cell ((GoB f),i0,(width (GoB f))) by A6, A7, A10, A11, A13, A14, A30, A49, A300, A302, GOBOARD5:28;
A304: left_cell (f,(k + 1)) = cell ((GoB f),i1,(width (GoB f))) by A4, A5, A13, A14, A16, A17, A30, A31, A49, A300, A301, A302, GOBOARD5:28;
A305: LSeg ((((1 / 2) * (((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f)))))) + |[0,1]|)) is connected by JORDAN1:6;
A306: LSeg ((((1 / 2) * (((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f)))))) + |[0,1]|)) meets Int (cell ((GoB f),i0,(width (GoB f)))) by A18, A21, A300, GOBOARD6:83;
LSeg ((((1 / 2) * (((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f)))))) + |[0,1]|)) misses L~ f by A18, A23, A51, A300, A301, GOBOARD8:28;
then LSeg ((((1 / 2) * (((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f)))))) + |[0,1]|)) c= (L~ f) ` by SUBSET_1:23;
then A307: LSeg ((((1 / 2) * (((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f)))))) + |[0,1]|)) c= LeftComp f by A3, A5, A6, A55, A303, A305, A306, Th6, NAT_1:13;
A308: LSeg ((((1 / 2) * (((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f)))))) + |[0,1]|)) meets Int (cell ((GoB f),i1,(width (GoB f)))) by A20, A23, A301, GOBOARD6:83;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A304, A307, A308, Th6, Th22; :: thesis: verum

end;

suppose that A309: i0 + 1 = i1 and
A310: i1 + 1 = i2 and
A311: j0 <> width (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A312: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A46, A309, GOBOARD5:28;
width (GoB f) > j0 by A25, A311, XXREAL_0:1;
then A313: width (GoB f) >= j0 + 1 by NAT_1:13;
A314: left_cell (f,(k + 1)) = cell ((GoB f),i1,j1) by A4, A5, A13, A14, A16, A17, A31, A46, A310, GOBOARD5:28;
A315: LSeg (((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),(j0 + 1))))),((1 / 2) * (((GoB f) * (i1,j0)) + ((GoB f) * ((i1 + 1),(j0 + 1)))))) is connected by JORDAN1:6;
A316: LSeg (((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),(j0 + 1))))),((1 / 2) * (((GoB f) * (i1,j0)) + ((GoB f) * ((i1 + 1),(j0 + 1)))))) meets Int (cell ((GoB f),i0,j1)) by A18, A21, A26, A30, A309, A313, GOBOARD6:82;
LSeg (((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),(j0 + 1))))),((1 / 2) * (((GoB f) * (i1,j0)) + ((GoB f) * ((i1 + 1),(j0 + 1)))))) misses L~ f by A5, A6, A11, A14, A17, A18, A23, A24, A30, A31, A50, A51, A309, A310, A313, GOBOARD8:14;
then LSeg (((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),(j0 + 1))))),((1 / 2) * (((GoB f) * (i1,j0)) + ((GoB f) * ((i1 + 1),(j0 + 1)))))) c= (L~ f) ` by SUBSET_1:23;
then A317: LSeg (((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),(j0 + 1))))),((1 / 2) * (((GoB f) * (i1,j0)) + ((GoB f) * ((i1 + 1),(j0 + 1)))))) c= LeftComp f by A3, A5, A6, A55, A312, A315, A316, Th6, NAT_1:13;
A318: LSeg (((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),(j0 + 1))))),((1 / 2) * (((GoB f) * (i1,j0)) + ((GoB f) * ((i1 + 1),(j0 + 1)))))) meets Int (cell ((GoB f),i1,j1)) by A20, A23, A24, A30, A309, A310, A313, GOBOARD6:82;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A314, A317, A318, Th6, Th22; :: thesis: verum

end;

suppose that A319: i0 + 1 = i1 and
A320: j1 + 1 = j2 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A46, A319, GOBOARD5:28
.= left_cell (f,(k + 1)) by A4, A5, A13, A14, A16, A17, A31, A319, A320, GOBOARD5:27 ;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A3, A5, A6, NAT_1:13; :: thesis: verum

end;

suppose that A321: j0 + 1 = j1 and
A322: i1 + 1 = i2 and
A323: i0 = 1 and
A324: j1 = width (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A325: left_cell (f,k) = cell ((GoB f),(i1 -' 1),j0) by A6, A7, A10, A11, A13, A14, A30, A45, A321, GOBOARD5:27;
A326: i0 -' 1 = 0 by A323, XREAL_1:232;
A327: j1 -' 1 = j0 by A321, NAT_D:34;
A328: LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((GoB f) * (1,j1)) + |[(- 1),1]|)) is connected by JORDAN1:6;
A329: LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((GoB f) * (1,j1)) + |[(- 1),1]|)) meets Int (cell ((GoB f),(i1 -' 1),j0)) by A24, A27, A30, A321, A326, GOBOARD6:85;
LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((GoB f) * (1,j1)) + |[(- 1),1]|)) misses L~ f by A324, A327, GOBOARD8:33;
then LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((GoB f) * (1,j1)) + |[(- 1),1]|)) c= (L~ f) ` by SUBSET_1:23;
then A330: LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((GoB f) * (1,j1)) + |[(- 1),1]|)) c= LeftComp f by A3, A5, A6, A55, A325, A328, A329, Th6, NAT_1:13;
i1 -' 1 <= i1 by NAT_D:35;
then A331: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2;
A332: LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((GoB f) * (1,j1)) + |[(- 1),1]|)) meets Int (cell ((GoB f),(i0 -' 1),j1)) by A324, A326, GOBOARD6:89;
Int (cell ((GoB f),(i1 -' 1),j1)) misses L~ f by A27, A331, GOBOARD7:12;
then Int (cell ((GoB f),(i1 -' 1),j1)) c= (L~ f) ` by SUBSET_1:23;
then A333: Int (cell ((GoB f),(i1 -' 1),j1)) c= LeftComp f by A27, A30, A55, A321, A330, A331, A332, Th6, Th21;
A334: left_cell (f,(k + 1)) = cell ((GoB f),i1,j1) by A4, A5, A13, A14, A16, A17, A31, A321, A322, GOBOARD5:28;
A335: LSeg ((((GoB f) * (1,j1)) + |[(- 1),1]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (2,j1)))) + |[0,1]|)) meets Int (cell ((GoB f),(i1 -' 1),j1)) by A30, A321, A324, A326, GOBOARD6:89;
LSeg ((((GoB f) * (1,j1)) + |[(- 1),1]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (2,j1)))) + |[0,1]|)) misses L~ f by A324, GOBOARD8:29;
then LSeg ((((GoB f) * (1,j1)) + |[(- 1),1]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (2,j1)))) + |[0,1]|)) c= (L~ f) ` by SUBSET_1:23;
then A336: LSeg ((((GoB f) * (1,j1)) + |[(- 1),1]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (2,j1)))) + |[0,1]|)) c= LeftComp f by A55, A333, A335, Th6, JORDAN1:6;
A337: LSeg ((((GoB f) * (1,j1)) + |[(- 1),1]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (2,j1)))) + |[0,1]|)) meets Int (cell ((GoB f),i1,j1)) by A23, A30, A321, A322, A323, A324, GOBOARD6:83;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A334, A336, A337, Th6, Th22; :: thesis: verum

end;

suppose that A338: j0 + 1 = j1 and
A339: i1 + 1 = i2 and
A340: i0 <> 1 and
A341: j1 = width (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A342: left_cell (f,k) = cell ((GoB f),(i1 -' 1),j0) by A6, A7, A10, A11, A13, A14, A30, A45, A338, GOBOARD5:27;
1 < i0 by A18, A340, XXREAL_0:1;
then A343: 1 <= i0 -' 1 by A30, A45, A338, NAT_1:13;
A344: j1 -' 1 = j0 by A338, NAT_D:34;
A345: (i1 -' 1) + (1 + 1) = i2 by A45, A339;
A346: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j0)) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|)) is connected by JORDAN1:6;
A347: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j0)) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|)) meets Int (cell ((GoB f),(i1 -' 1),j0)) by A21, A24, A27, A30, A45, A338, A343, GOBOARD6:82;
LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j0)) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|)) misses L~ f by A5, A6, A11, A14, A17, A23, A30, A31, A45, A50, A338, A341, A343, A344, A345, GOBOARD8:9;
then LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j0)) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|)) c= (L~ f) ` by SUBSET_1:23;
then A348: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j0)) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|)) c= LeftComp f by A3, A5, A6, A55, A342, A346, A347, Th6, NAT_1:13;
i1 -' 1 <= i1 by NAT_D:35;
then A349: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2;
A350: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j0)) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|)) meets Int (cell ((GoB f),(i0 -' 1),j1)) by A19, A30, A45, A338, A341, A343, GOBOARD6:83;
Int (cell ((GoB f),(i1 -' 1),j1)) misses L~ f by A27, A349, GOBOARD7:12;
then Int (cell ((GoB f),(i1 -' 1),j1)) c= (L~ f) ` by SUBSET_1:23;
then A351: Int (cell ((GoB f),(i1 -' 1),j1)) c= LeftComp f by A27, A30, A55, A338, A348, A349, A350, Th6, Th21;
A352: left_cell (f,(k + 1)) = cell ((GoB f),i1,j1) by A4, A5, A13, A14, A16, A17, A31, A338, A339, GOBOARD5:28;
A353: LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,j1)))) + |[0,1]|)) meets Int (cell ((GoB f),(i1 -' 1),j1)) by A21, A30, A45, A338, A341, A343, GOBOARD6:83;
LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,j1)))) + |[0,1]|)) misses L~ f by A23, A30, A45, A338, A341, A343, A345, GOBOARD8:28;
then LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,j1)))) + |[0,1]|)) c= (L~ f) ` by SUBSET_1:23;
then A354: LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,j1)))) + |[0,1]|)) c= LeftComp f by A55, A351, A353, Th6, JORDAN1:6;
A355: LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,j1)))) + |[0,1]|)) meets Int (cell ((GoB f),i1,j1)) by A20, A23, A339, A341, GOBOARD6:83;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A352, A354, A355, Th6, Th22; :: thesis: verum

end;

suppose that A356: j0 + 1 = j1 and
A357: i1 + 1 = i2 and
A358: i0 = 1 and
A359: j1 <> width (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A360: left_cell (f,k) = cell ((GoB f),(i1 -' 1),j0) by A6, A7, A10, A11, A13, A14, A30, A45, A356, GOBOARD5:27;
width (GoB f) > j1 by A27, A359, XXREAL_0:1;
then A361: width (GoB f) >= j1 + 1 by NAT_1:13;
A362: i0 -' 1 = 0 by A358, XREAL_1:232;
A363: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1))))) - |[1,0]|)) is connected by JORDAN1:6;
A364: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1))))) - |[1,0]|)) meets Int (cell ((GoB f),(i1 -' 1),j0)) by A24, A27, A30, A356, A358, A362, GOBOARD6:85;
LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1))))) - |[1,0]|)) misses L~ f by A24, A53, A356, A358, A361, GOBOARD8:31;
then LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1))))) - |[1,0]|)) c= (L~ f) ` by SUBSET_1:23;
then A365: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1))))) - |[1,0]|)) c= LeftComp f by A3, A5, A6, A55, A360, A363, A364, Th6, NAT_1:13;
i1 -' 1 <= i1 by NAT_D:35;
then A366: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2;
A367: LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1))))) - |[1,0]|)) meets Int (cell ((GoB f),(i0 -' 1),j1)) by A26, A358, A361, A362, GOBOARD6:85;
Int (cell ((GoB f),(i1 -' 1),j1)) misses L~ f by A27, A366, GOBOARD7:12;
then Int (cell ((GoB f),(i1 -' 1),j1)) c= (L~ f) ` by SUBSET_1:23;
then A368: Int (cell ((GoB f),(i1 -' 1),j1)) c= LeftComp f by A27, A30, A55, A356, A365, A366, A367, Th6, Th21;
A369: left_cell (f,(k + 1)) = cell ((GoB f),i1,j1) by A4, A5, A13, A14, A16, A17, A31, A356, A357, GOBOARD5:28;
A370: LSeg ((((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i1,(j0 + 2))))) - |[1,0]|),((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i2,(j0 + 2)))))) meets Int (cell ((GoB f),(i1 -' 1),j1)) by A26, A30, A356, A358, A361, A362, GOBOARD6:85;
LSeg ((((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i1,(j0 + 2))))) - |[1,0]|),((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i2,(j0 + 2)))))) misses L~ f by A5, A6, A11, A14, A17, A24, A30, A31, A50, A356, A357, A358, A361, GOBOARD8:18;
then LSeg ((((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i1,(j0 + 2))))) - |[1,0]|),((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i2,(j0 + 2)))))) c= (L~ f) ` by SUBSET_1:23;
then A371: LSeg ((((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i1,(j0 + 2))))) - |[1,0]|),((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i2,(j0 + 2)))))) c= LeftComp f by A55, A368, A370, Th6, JORDAN1:6;
A372: LSeg ((((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i1,(j0 + 2))))) - |[1,0]|),((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i2,(j0 + 2)))))) meets Int (cell ((GoB f),i1,j1)) by A20, A23, A26, A356, A357, A361, GOBOARD6:82;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A369, A371, A372, Th6, Th22; :: thesis: verum

end;

suppose that A373: j0 + 1 = j1 and
A374: i1 + 1 = i2 and
A375: i0 <> 1 and
A376: j1 <> width (GoB f) ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A377: left_cell (f,k) = cell ((GoB f),(i1 -' 1),j0) by A6, A7, A10, A11, A13, A14, A30, A45, A373, GOBOARD5:27;
1 < i0 by A18, A375, XXREAL_0:1;
then A378: 1 <= i0 -' 1 by A30, A45, A373, NAT_1:13;
width (GoB f) > j1 by A27, A376, XXREAL_0:1;
then A379: width (GoB f) >= j1 + 1 by NAT_1:13;
A380: (i1 -' 1) + (1 + 1) = i2 by A45, A374;
A381: LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,(j1 + 1)))))) is connected by JORDAN1:6;
A382: LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,(j1 + 1)))))) meets Int (cell ((GoB f),(i1 -' 1),j0)) by A21, A24, A27, A30, A45, A373, A378, GOBOARD6:82;
LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,(j1 + 1)))))) misses L~ f by A5, A6, A11, A14, A17, A23, A24, A30, A31, A45, A50, A53, A373, A378, A379, A380, GOBOARD8:3;
then LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,(j1 + 1)))))) c= (L~ f) ` by SUBSET_1:23;
then A383: LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,(j1 + 1)))))) c= LeftComp f by A3, A5, A6, A55, A377, A381, A382, Th6, NAT_1:13;
i1 -' 1 <= i1 by NAT_D:35;
then A384: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2;
A385: LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,(j1 + 1)))))) meets Int (cell ((GoB f),(i0 -' 1),j1)) by A19, A26, A30, A45, A373, A378, A379, GOBOARD6:82;
Int (cell ((GoB f),(i1 -' 1),j1)) misses L~ f by A27, A384, GOBOARD7:12;
then Int (cell ((GoB f),(i1 -' 1),j1)) c= (L~ f) ` by SUBSET_1:23;
then A386: Int (cell ((GoB f),(i1 -' 1),j1)) c= LeftComp f by A27, A30, A55, A373, A383, A384, A385, Th6, Th21;
A387: left_cell (f,(k + 1)) = cell ((GoB f),i1,j1) by A4, A5, A13, A14, A16, A17, A31, A373, A374, GOBOARD5:28;
A388: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,(j1 + 1))))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,(j1 + 1)))))) meets Int (cell ((GoB f),(i1 -' 1),j1)) by A21, A26, A30, A45, A373, A378, A379, GOBOARD6:82;
LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,(j1 + 1))))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,(j1 + 1)))))) misses L~ f by A5, A6, A11, A14, A17, A23, A24, A30, A31, A45, A50, A53, A373, A378, A379, A380, GOBOARD8:15;
then LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,(j1 + 1))))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,(j1 + 1)))))) c= (L~ f) ` by SUBSET_1:23;
then A389: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,(j1 + 1))))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,(j1 + 1)))))) c= LeftComp f by A55, A386, A388, Th6, JORDAN1:6;
A390: LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,(j1 + 1))))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,(j1 + 1)))))) meets Int (cell ((GoB f),i1,j1)) by A20, A23, A26, A374, A379, GOBOARD6:82;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A387, A389, A390, Th6, Th22; :: thesis: verum

end;

suppose that A391: j0 + 1 = j1 and
A392: j1 + 1 = j2 and
A393: i0 = 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A394: left_cell (f,k) = cell ((GoB f),0,j0) by A6, A7, A10, A11, A13, A14, A30, A56, A391, A393, GOBOARD5:27;
A395: left_cell (f,(k + 1)) = cell ((GoB f),0,j1) by A4, A5, A13, A14, A16, A17, A30, A31, A56, A391, A392, A393, GOBOARD5:27;
A396: LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (1,j2)))) - |[1,0]|)) is connected by JORDAN1:6;
A397: LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (1,j2)))) - |[1,0]|)) meets Int (cell ((GoB f),0,j0)) by A24, A27, A391, GOBOARD6:85;
LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (1,j2)))) - |[1,0]|)) misses L~ f by A24, A29, A53, A391, A392, GOBOARD8:31;
then LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (1,j2)))) - |[1,0]|)) c= (L~ f) ` by SUBSET_1:23;
then A398: LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (1,j2)))) - |[1,0]|)) c= LeftComp f by A3, A5, A6, A55, A394, A396, A397, Th6, NAT_1:13;
A399: LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (1,j2)))) - |[1,0]|)) meets Int (cell ((GoB f),0,j1)) by A26, A29, A392, GOBOARD6:85;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A55, A395, A398, A399, Th6, Th22; :: thesis: verum

end;

suppose that A400: j0 + 1 = j1 and
A401: j1 + 1 = j2 and
A402: i0 <> 1 ; :: thesis: Int (left_cell (f,(k + 1))) c= LeftComp f

A403: left_cell (f,k) = cell ((GoB f),(i1 -' 1),j0) by A6, A7, A10, A11, A13, A14, A30, A45, A400, GOBOARD5:27;
1 < i0 by A18, A402, XXREAL_0:1;
then A404: 1 <= i0 -' 1 by A30, A45, A400, NAT_1:13;
A405: left_cell (f,(k + 1)) = cell ((GoB f),(i1 -' 1),j1) by A4, A5, A13, A14, A16, A17, A31, A45, A401, GOBOARD5:27;
A406: LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,j2))))) is connected by JORDAN1:6;
A407: LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,j2))))) meets Int (cell ((GoB f),(i1 -' 1),j0)) by A21, A24, A27, A30, A45, A400, A404, GOBOARD6:82;
LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,j2))))) misses L~ f by A5, A6, A11, A14, A17, A19, A24, A29, A30, A31, A45, A50, A53, A400, A401, A404, GOBOARD8:1;
then LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,j2))))) c= (L~ f) ` by SUBSET_1:23;
then A408: LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,j2))))) c= LeftComp f by A3, A5, A6, A55, A403, A406, A407, Th6, NAT_1:13;
A409: LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,j2))))) meets Int (cell ((GoB f),(i0 -' 1),j1)) by A19, A26, A29, A30, A45, A400, A401, A404, GOBOARD6:82;
Int (left_cell (f,(k + 1))) misses L~ f by A4, A5, GOBOARD8:37;
then Int (left_cell (f,(k + 1))) c= (L~ f) ` by SUBSET_1:23;
hence Int (left_cell (f,(k + 1))) c= LeftComp f by A4, A5, A30, A55, A400, A405, A408, A409, Th6, Th22; :: thesis: verum

end;

end;

end;

hence Int (left_cell (f,(k + 1))) c= LeftComp f ; :: thesis: verum

end;

end;

end;

end;

thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A2); :: thesis: verum