:: GOBOARD9 semantic presentation

begin


theorem Th1: :: GOBOARD9:1
for GX being TopSpace
for A1, A2, B being Subset of GX st A1 is_a_component_of B & A2 is_a_component_of B & not A1 = A2 holds
A1 misses A2
proof
let GX be TopSpace; ::_thesis: for A1, A2, B being Subset of GX st A1 is_a_component_of B & A2 is_a_component_of B & not A1 = A2 holds
A1 misses A2
let A1, A2, B be Subset of GX; ::_thesis: ( A1 is_a_component_of B & A2 is_a_component_of B & not A1 = A2 implies A1 misses A2 )
assume  A1 is_a_component_of B ; ::_thesis: ( not A2 is_a_component_of B or A1 = A2 or A1 misses A2 )
then A1: ex B1 being Subset of (GX | B) st
( B1 = A1 & B1 is a_component ) by CONNSP_1:def_6;
assume  A2 is_a_component_of B ; ::_thesis: ( A1 = A2 or A1 misses A2 )
then  ex B2 being Subset of (GX | B) st
( B2 = A2 & B2 is a_component ) by CONNSP_1:def_6;
hence  ( A1 = A2 or A1 misses A2 ) by A1, CONNSP_1:35; ::_thesis: verum
end;

theorem Th2: :: GOBOARD9:2
for GX being TopSpace
for A, B being Subset of GX
for AA being Subset of (GX | B) st A = AA holds
GX | A = (GX | B) | AA
proof
let GX be TopSpace; ::_thesis: for A, B being Subset of GX
for AA being Subset of (GX | B) st A = AA holds
GX | A = (GX | B) | AA
let A, B be Subset of GX; ::_thesis: for AA being Subset of (GX | B) st A = AA holds
GX | A = (GX | B) | AA
let AA be Subset of (GX | B); ::_thesis: ( A = AA implies GX | A = (GX | B) | AA )
assume A1: A = AA ; ::_thesis: GX | A = (GX | B) | AA
the carrier of (GX | A) = [#] (GX | A)
.= A by PRE_TOPC:def_5 ;
then reconsider GY = GX | A as strict SubSpace of GX | B by A1, TSEP_1:4;
 [#] GY = AA by A1, PRE_TOPC:def_5;
hence  GX | A = (GX | B) | AA by PRE_TOPC:def_5; ::_thesis: verum
end;

theorem Th3: :: GOBOARD9:3
for GX being non empty TopSpace
for A, B being non empty Subset of GX st A c= B & A is connected holds
ex C being Subset of GX st
( C is_a_component_of B & A c= C )
proof
let GX be non empty TopSpace; ::_thesis: for A, B being non empty Subset of GX st A c= B & A is connected holds
ex C being Subset of GX st
( C is_a_component_of B & A c= C )
let A, B be non empty Subset of GX; ::_thesis: ( A c= B & A is connected implies ex C being Subset of GX st
( C is_a_component_of B & A c= C ) )
assume that
A1: A c= B and
A2: A is connected ; ::_thesis: ex C being Subset of GX st
( C is_a_component_of B & A c= C )
consider p being set  such that
A3: p in A by XBOOLE_0:def_1;
A4: B = [#] (GX | B) by PRE_TOPC:def_5
.= the carrier of (GX | B) ;
then reconsider p = p as Point of (GX | B) by A1, A3;
reconsider C = Component_of p as Subset of GX by PRE_TOPC:11;
take  C ; ::_thesis: ( C is_a_component_of B & A c= C )
A5: Component_of p is a_component by CONNSP_1:40;
hence  C is_a_component_of B by CONNSP_1:def_6; ::_thesis: A c= C
reconsider AA = A as Subset of (GX | B) by A1, A4;
 GX | A is connected by A2, CONNSP_1:def_3;
then  (GX | B) | AA is connected by Th2;
then A6: AA is connected by CONNSP_1:def_3;
 p in Component_of p by CONNSP_1:38;
then  AA /\ (Component_of p) <> {} (GX | B) by A3, XBOOLE_0:def_4;
then  AA meets Component_of p by XBOOLE_0:def_7;
hence  A c= C by A5, A6, CONNSP_1:36; ::_thesis: verum
end;

theorem Th4: :: GOBOARD9:4
for GX being non empty TopSpace
for A, B, C, D being Subset of GX st B is connected & C is_a_component_of D & A c= C & A meets B & B c= D holds
B c= C
proof
let GX be non empty TopSpace; ::_thesis: for A, B, C, D being Subset of GX st B is connected & C is_a_component_of D & A c= C & A meets B & B c= D holds
B c= C
let A, B, C, D be Subset of GX; ::_thesis: ( B is connected & C is_a_component_of D & A c= C & A meets B & B c= D implies B c= C )
assume that
A1: B is connected and
A2: C is_a_component_of D and
A3: A c= C and
A4: A meets B and
A5: B c= D ; ::_thesis: B c= C
A6: A <> {} by A4, XBOOLE_1:65;
A7: B <> {} by A4, XBOOLE_1:65;
reconsider A = A, B = B as non empty Subset of GX by A4, XBOOLE_1:65;
reconsider C = C, D = D as non empty Subset of GX by A3, A5, A6, A7, XBOOLE_1:3;
consider CC being Subset of GX such that
A8: CC is_a_component_of D and
A9: B c= CC by A1, A5, Th3;
A10: A meets CC by A4, A9, XBOOLE_1:63;
A11: ex C1 being Subset of (GX | D) st
( C1 = C & C1 is a_component ) by A2, CONNSP_1:def_6;
 ex CC1 being Subset of (GX | D) st
( CC1 = CC & CC1 is a_component ) by A8, CONNSP_1:def_6;
hence  B c= C by A3, A9, A10, A11, CONNSP_1:35, XBOOLE_1:63; ::_thesis: verum
end;

registration
cluster non empty convex for Element of K6( the carrier of (TOP-REAL 2));
existence
 ex b1 being Subset of (TOP-REAL 2) st
( b1 is convex & not b1 is empty )
proof
set p = the Point of (TOP-REAL 2);
take  LSeg ( the Point of (TOP-REAL 2), the Point of (TOP-REAL 2)) ; ::_thesis: ( LSeg ( the Point of (TOP-REAL 2), the Point of (TOP-REAL 2)) is convex & not LSeg ( the Point of (TOP-REAL 2), the Point of (TOP-REAL 2)) is empty )
thus  ( LSeg ( the Point of (TOP-REAL 2), the Point of (TOP-REAL 2)) is convex & not LSeg ( the Point of (TOP-REAL 2), the Point of (TOP-REAL 2)) is empty ) ; ::_thesis: verum
end;
end;

theorem :: GOBOARD9:5
canceled;

theorem Th6: :: GOBOARD9:6
for P, Q being convex Subset of (TOP-REAL 2) holds P /\ Q is convex
proof
let P, Q be convex Subset of (TOP-REAL 2); ::_thesis: P /\ Q is convex
let p be Point of (TOP-REAL 2); :: according to JORDAN1:def_1 ::_thesis: for b1 being Element of the carrier of (TOP-REAL 2) holds
( not p in P /\ Q or not b1 in P /\ Q or LSeg (p,b1) c= P /\ Q )
let q be Point of (TOP-REAL 2); ::_thesis: ( not p in P /\ Q or not q in P /\ Q or LSeg (p,q) c= P /\ Q )
assume that
A1: p in P /\ Q and
A2: q in P /\ Q ; ::_thesis: LSeg (p,q) c= P /\ Q
A3: p in P by A1, XBOOLE_0:def_4;
 q in P by A2, XBOOLE_0:def_4;
then A4: LSeg (p,q) c= P by A3, JORDAN1:def_1;
A5: p in Q by A1, XBOOLE_0:def_4;
 q in Q by A2, XBOOLE_0:def_4;
then  LSeg (p,q) c= Q by A5, JORDAN1:def_1;
hence  LSeg (p,q) c= P /\ Q by A4, XBOOLE_1:19; ::_thesis: verum
end;

theorem Th7: :: GOBOARD9:7
for f being FinSequence of (TOP-REAL 2) holds Rev (X_axis f) = X_axis (Rev f)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: Rev (X_axis f) = X_axis (Rev f)
A1: len (Rev (X_axis f)) = len (X_axis f) by FINSEQ_5:def_3
.= len f by GOBOARD1:def_1
.= len (Rev f) by FINSEQ_5:def_3 ;
 len (X_axis f) = len f by GOBOARD1:def_1;
then A2: dom (X_axis f) = dom f by FINSEQ_3:29;
A3: len f = len (Rev f) by FINSEQ_5:def_3;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_(Rev_(X_axis_f))_holds_
(Rev_(X_axis_f))_._k_=_((Rev_f)_/._k)_`1
let k be Element of NAT ; ::_thesis: ( k in dom (Rev (X_axis f)) implies (Rev (X_axis f)) . k = ((Rev f) /. k) `1 )
assume A4: k in dom (Rev (X_axis f)) ; ::_thesis: (Rev (X_axis f)) . k = ((Rev f) /. k) `1
set l = ((len f) + 1) -' k;
A5: k <= len f by A1, A3, A4, FINSEQ_3:25;
 len f < (len f) + 1 by NAT_1:13;
then A6: (((len f) + 1) -' k) + k = (len f) + 1 by A5, XREAL_1:235, XXREAL_0:2;
A7: Rev (Rev (X_axis f)) = X_axis f ;
then A8: ((len f) + 1) -' k in dom (X_axis f) by A1, A3, A4, A6, FINSEQ_5:59;
thus (Rev (X_axis f)) . k = (Rev (X_axis f)) /. k by A4, PARTFUN1:def_6
.= (X_axis f) /. (((len f) + 1) -' k) by A1, A3, A4, A6, A7, FINSEQ_5:66
.= (X_axis f) . (((len f) + 1) -' k) by A8, PARTFUN1:def_6
.= (f /. (((len f) + 1) -' k)) `1 by A8, GOBOARD1:def_1
.= ((Rev f) /. k) `1 by A1, A2, A3, A4, A6, A7, FINSEQ_5:59, FINSEQ_5:66 ; ::_thesis: verum
end;
hence  Rev (X_axis f) = X_axis (Rev f) by A1, GOBOARD1:def_1; ::_thesis: verum
end;

theorem Th8: :: GOBOARD9:8
for f being FinSequence of (TOP-REAL 2) holds Rev (Y_axis f) = Y_axis (Rev f)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: Rev (Y_axis f) = Y_axis (Rev f)
A1: len (Rev (Y_axis f)) = len (Y_axis f) by FINSEQ_5:def_3
.= len f by GOBOARD1:def_2
.= len (Rev f) by FINSEQ_5:def_3 ;
 len (Y_axis f) = len f by GOBOARD1:def_2;
then A2: dom (Y_axis f) = dom f by FINSEQ_3:29;
A3: len f = len (Rev f) by FINSEQ_5:def_3;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_(Rev_(Y_axis_f))_holds_
(Rev_(Y_axis_f))_._k_=_((Rev_f)_/._k)_`2
let k be Element of NAT ; ::_thesis: ( k in dom (Rev (Y_axis f)) implies (Rev (Y_axis f)) . k = ((Rev f) /. k) `2 )
assume A4: k in dom (Rev (Y_axis f)) ; ::_thesis: (Rev (Y_axis f)) . k = ((Rev f) /. k) `2
set l = ((len f) + 1) -' k;
A5: k <= len f by A1, A3, A4, FINSEQ_3:25;
 len f < (len f) + 1 by NAT_1:13;
then A6: (((len f) + 1) -' k) + k = (len f) + 1 by A5, XREAL_1:235, XXREAL_0:2;
A7: Rev (Rev (Y_axis f)) = Y_axis f ;
then A8: ((len f) + 1) -' k in dom (Y_axis f) by A1, A3, A4, A6, FINSEQ_5:59;
thus (Rev (Y_axis f)) . k = (Rev (Y_axis f)) /. k by A4, PARTFUN1:def_6
.= (Y_axis f) /. (((len f) + 1) -' k) by A1, A3, A4, A6, A7, FINSEQ_5:66
.= (Y_axis f) . (((len f) + 1) -' k) by A8, PARTFUN1:def_6
.= (f /. (((len f) + 1) -' k)) `2 by A8, GOBOARD1:def_2
.= ((Rev f) /. k) `2 by A1, A2, A3, A4, A6, A7, FINSEQ_5:59, FINSEQ_5:66 ; ::_thesis: verum
end;
hence  Rev (Y_axis f) = Y_axis (Rev f) by A1, GOBOARD1:def_2; ::_thesis: verum
end;

Lm1:  for f, ff being non empty FinSequence of (TOP-REAL 2) st ff = Rev f holds
GoB ff = GoB f
proof
let f, ff be non empty FinSequence of (TOP-REAL 2); ::_thesis: ( ff = Rev f implies GoB ff = GoB f )
assume A1: ff = Rev f ; ::_thesis: GoB ff = GoB f
then A2: Rev (X_axis f) = X_axis ff by Th7;
A3: rng (Incr (X_axis ff)) = rng (X_axis ff) by SEQ_4:def_21
.= rng (X_axis f) by A2, FINSEQ_5:57 ;
len (Incr (X_axis ff)) = card (rng (X_axis ff)) by SEQ_4:def_21
.= card (rng (X_axis f)) by A2, FINSEQ_5:57 ;
then A4: Incr (X_axis f) = Incr (X_axis ff) by A3, SEQ_4:def_21;
A5: Rev (Y_axis f) = Y_axis ff by A1, Th8;
A6: rng (Incr (Y_axis ff)) = rng (Y_axis ff) by SEQ_4:def_21
.= rng (Y_axis f) by A5, FINSEQ_5:57 ;
len (Incr (Y_axis ff)) = card (rng (Y_axis ff)) by SEQ_4:def_21
.= card (rng (Y_axis f)) by A5, FINSEQ_5:57 ;
then  Incr (Y_axis f) = Incr (Y_axis ff) by A6, SEQ_4:def_21;
hence  GoB ff = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by A4, GOBOARD2:def_2
.= GoB f by GOBOARD2:def_2 ;
::_thesis: verum
end;

registration
clusterV13() V16( NAT ) Function-like non constant V26() FinSequence-like FinSubsequence-like for set ;
existence
 not for b1 being FinSequence holds b1 is constant
proof
take  <*1,2*> ; ::_thesis: not <*1,2*> is constant
take  1 ; :: according to SEQM_3:def_10 ::_thesis: ex b1 being Element of NAT st
( 1 in dom <*1,2*> & b1 in dom <*1,2*> & not <*1,2*> . 1 = <*1,2*> . b1 )
take  2 ; ::_thesis: ( 1 in dom <*1,2*> & 2 in dom <*1,2*> & not <*1,2*> . 1 = <*1,2*> . 2 )
A1: 1 in {1,2} by TARSKI:def_2;
 2 in {1,2} by TARSKI:def_2;
hence  ( 1 in dom <*1,2*> & 2 in dom <*1,2*> ) by A1, FINSEQ_1:2, FINSEQ_1:89; ::_thesis: not <*1,2*> . 1 = <*1,2*> . 2
 <*1,2*> . 1 = 1 by FINSEQ_1:44;
hence  not <*1,2*> . 1 = <*1,2*> . 2 by FINSEQ_1:44; ::_thesis: verum
end;
end;

registration
let f be non constant FinSequence;
cluster Rev f ->  non constant ;
coherence
 not Rev f is constant
proof
consider i, j being Element of NAT  such that
A1: i in dom f and
A2: j in dom f and
A3: f . i <> f . j by SEQM_3:def_10;
A4: i <= len f by A1, FINSEQ_3:25;
 j <= len f by A2, FINSEQ_3:25;
then reconsider k1 = (len f) - i, l1 = (len f) - j as Element of NAT by A4, INT_1:5;
take k = k1 + 1; :: according to SEQM_3:def_10 ::_thesis: ex b1 being Element of NAT st
( k in dom (Rev f) & b1 in dom (Rev f) & not (Rev f) . k = (Rev f) . b1 )
take l = l1 + 1; ::_thesis: ( k in dom (Rev f) & l in dom (Rev f) & not (Rev f) . k = (Rev f) . l )
 k + i = (len f) + 1 ;
hence  k in dom (Rev f) by A1, FINSEQ_5:59; ::_thesis: ( l in dom (Rev f) & not (Rev f) . k = (Rev f) . l )
then A5: (Rev f) . k = f . (((len f) - k) + 1) by FINSEQ_5:def_3
.= f . (0 + i) ;
 l + j = (len f) + 1 ;
hence  l in dom (Rev f) by A2, FINSEQ_5:59; ::_thesis: not (Rev f) . k = (Rev f) . l
then (Rev f) . l = f . (((len f) - l) + 1) by FINSEQ_5:def_3
.= f . (0 + j) ;
hence  not (Rev f) . k = (Rev f) . l by A3, A5; ::_thesis: verum
end;
end;

definition
let f be standard special_circular_sequence;
:: original: Rev
redefine func Rev f ->  standard special_circular_sequence;
coherence
 Rev f is standard special_circular_sequence
proof
reconsider ff = Rev f as non empty FinSequence of (TOP-REAL 2) ;
A1: Rev ff = f ;
A2: GoB ff = GoB f by Lm1;
A3: f is_sequence_on GoB f by GOBOARD5:def_5;
A4: len f = len ff by FINSEQ_5:def_3;
A5: ff is standard
proof
hereby  :: according to GOBOARD5:def_5,GOBOARD1:def_9 ::_thesis: for b1 being Element of NAT holds
( not b1 in dom ff or not b1 + 1 in dom ff or for b2, b3, b4, b5 being Element of NAT holds
( not [b2,b3] in Indices (GoB ff) or not [b4,b5] in Indices (GoB ff) or not ff /. b1 = (GoB ff) * (b2,b3) or not ff /. (b1 + 1) = (GoB ff) * (b4,b5) or K36((abs K40(b2,b4)),(abs K40(b3,b5))) = 1 ) )
let k be Element of NAT ; ::_thesis: ( k in dom ff implies ex i, j being Element of NAT st
( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) ) )
assume A6: k in dom ff ; ::_thesis: ex i, j being Element of NAT st
( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) )
set l = ((len f) + 1) -' k;
A7: k <= len f by A4, A6, FINSEQ_3:25;
 len f < (len f) + 1 by NAT_1:13;
then A8: (((len f) + 1) -' k) + k = (len f) + 1 by A7, XREAL_1:235, XXREAL_0:2;
then  ((len f) + 1) -' k in dom f by A1, A4, A6, FINSEQ_5:59;
then consider i, j being Element of NAT  such that
A9: [i,j] in Indices (GoB f) and
A10: f /. (((len f) + 1) -' k) = (GoB f) * (i,j) by A3, GOBOARD1:def_9;
take i = i; ::_thesis: ex j being Element of NAT st
( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) )
take j = j; ::_thesis: ( [i,j] in Indices (GoB ff) & ff /. k = (GoB ff) * (i,j) )
thus  [i,j] in Indices (GoB ff) by A9, Lm1; ::_thesis: ff /. k = (GoB ff) * (i,j)
thus  ff /. k = (GoB ff) * (i,j) by A1, A2, A4, A6, A8, A10, FINSEQ_5:66; ::_thesis: verum
end;
let k be Element of NAT ; ::_thesis: ( not k in dom ff or not k + 1 in dom ff or for b1, b2, b3, b4 being Element of NAT holds
( not [b1,b2] in Indices (GoB ff) or not [b3,b4] in Indices (GoB ff) or not ff /. k = (GoB ff) * (b1,b2) or not ff /. (k + 1) = (GoB ff) * (b3,b4) or K36((abs K40(b1,b3)),(abs K40(b2,b4))) = 1 ) )
assume that
A11: k in dom ff and
A12: k + 1 in dom ff ; ::_thesis: for b1, b2, b3, b4 being Element of NAT holds
( not [b1,b2] in Indices (GoB ff) or not [b3,b4] in Indices (GoB ff) or not ff /. k = (GoB ff) * (b1,b2) or not ff /. (k + 1) = (GoB ff) * (b3,b4) or K36((abs K40(b1,b3)),(abs K40(b2,b4))) = 1 )
set l = ((len f) + 1) -' (k + 1);
 k <= len f by A4, A11, FINSEQ_3:25;
then  k + 1 <= (len f) + 1 by XREAL_1:6;
then A13: (((len f) + 1) -' (k + 1)) + (k + 1) = (len f) + 1 by XREAL_1:235;
then A14: ((len f) + 1) -' (k + 1) in dom f by A1, A4, A12, FINSEQ_5:59;
A15: ((((len f) + 1) -' (k + 1)) + 1) + k = (len f) + 1 by A13;
then A16: (((len f) + 1) -' (k + 1)) + 1 in dom f by A1, A4, A11, FINSEQ_5:59;
let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( not [i1,j1] in Indices (GoB ff) or not [i2,j2] in Indices (GoB ff) or not ff /. k = (GoB ff) * (i1,j1) or not ff /. (k + 1) = (GoB ff) * (i2,j2) or K36((abs K40(i1,i2)),(abs K40(j1,j2))) = 1 )
assume that
A17: [i1,j1] in Indices (GoB ff) and
A18: [i2,j2] in Indices (GoB ff) and
A19: ff /. k = (GoB ff) * (i1,j1) and
A20: ff /. (k + 1) = (GoB ff) * (i2,j2) ; ::_thesis: K36((abs K40(i1,i2)),(abs K40(j1,j2))) = 1
A21: abs (i2 - i1) = abs (- (i1 - i2))
.= abs (i1 - i2) by COMPLEX1:52 ;
A22: abs (j2 - j1) = abs (- (j1 - j2))
.= abs (j1 - j2) by COMPLEX1:52 ;
A23: f /. (((len f) + 1) -' (k + 1)) = (GoB f) * (i2,j2) by A1, A2, A4, A12, A13, A20, FINSEQ_5:66;
 f /. ((((len f) + 1) -' (k + 1)) + 1) = (GoB f) * (i1,j1) by A1, A2, A4, A11, A15, A19, FINSEQ_5:66;
hence  (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A2, A3, A14, A16, A17, A18, A21, A22, A23, GOBOARD1:def_9; ::_thesis: verum
end;
A24: ff /. 1 = f /. (len f) by FINSEQ_5:65
.= f /. 1 by FINSEQ_6:def_1
.= ff /. (len ff) by A4, FINSEQ_5:65 ;
 ff is s.c.c.
proof
let i be Element of NAT ; :: according to GOBOARD5:def_4 ::_thesis: for b1 being Element of NAT holds
( b1 <= i + 1 or ( ( i <= 1 or len ff <= b1 ) & len ff <= b1 + 1 ) or LSeg (ff,i) misses LSeg (ff,b1) )
let j be Element of NAT ; ::_thesis: ( j <= i + 1 or ( ( i <= 1 or len ff <= j ) & len ff <= j + 1 ) or LSeg (ff,i) misses LSeg (ff,j) )
assume that
A25: i + 1 < j and
A26: ( ( i > 1 & j < len ff ) or j + 1 < len ff ) ; ::_thesis: LSeg (ff,i) misses LSeg (ff,j)
set k = (len f) -' i;
set l = (len f) -' j;
A27: j <= len f by A4, A26, NAT_1:13;
then A28: ((len f) -' j) + j = len f by XREAL_1:235;
 i < j by A25, NAT_1:13;
then A29: ((len f) -' i) + i = len f by A27, XREAL_1:235, XXREAL_0:2;
then  (i + 1) + ((len f) -' i) = (((len f) -' j) + 1) + j by A28;
then  (((len f) -' j) + 1) + j < j + ((len f) -' i) by A25, XREAL_1:6;
then A30: ((len f) -' j) + 1 < (len f) -' i by XREAL_1:6;
A31: j + 1 <= len f by A4, A26, NAT_1:13;
percases ( j + 1 = len f or ( i >= 1 & j + 1 < len f ) or i = 0 ) by A31, NAT_1:14, XXREAL_0:1;
suppose j + 1 = len f ; ::_thesis: LSeg (ff,i) misses LSeg (ff,j)
then  ((len f) -' i) + 1 < len f by A26, A29, FINSEQ_5:def_3, XREAL_1:6;
then  LSeg (f,((len f) -' i)) misses LSeg (f,((len f) -' j)) by A30, GOBOARD5:def_4;
then A32: (LSeg (f,((len f) -' i))) /\ (LSeg (f,((len f) -' j))) = {} by XBOOLE_0:def_7;
 LSeg (f,((len f) -' i)) = LSeg (ff,i) by A29, SPPOL_2:2;
hence  (LSeg (ff,i)) /\ (LSeg (ff,j)) = {} by A28, A32, SPPOL_2:2; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
supposethat A33: i >= 1 and
A34: j + 1 < len f ; ::_thesis: LSeg (ff,i) misses LSeg (ff,j)
A35: (len f) -' j > 1 by A28, A34, XREAL_1:6;
 ((len f) -' i) + 1 <= len f by A29, A33, XREAL_1:6;
then  (len f) -' i < len f by NAT_1:13;
then  LSeg (f,((len f) -' i)) misses LSeg (f,((len f) -' j)) by A30, A35, GOBOARD5:def_4;
then A36: (LSeg (f,((len f) -' i))) /\ (LSeg (f,((len f) -' j))) = {} by XBOOLE_0:def_7;
 LSeg (f,((len f) -' i)) = LSeg (ff,i) by A29, SPPOL_2:2;
hence  (LSeg (ff,i)) /\ (LSeg (ff,j)) = {} by A28, A36, SPPOL_2:2; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
suppose i = 0 ; ::_thesis: LSeg (ff,i) misses LSeg (ff,j)
then  LSeg (ff,i) = {} by TOPREAL1:def_3;
hence  (LSeg (ff,i)) /\ (LSeg (ff,j)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
end;
end;
hence  Rev f is standard special_circular_sequence by A5, A24, FINSEQ_6:def_1, SPPOL_2:28, SPPOL_2:40; ::_thesis: verum
end;
end;

theorem Th9: :: GOBOARD9:9
for f being non constant standard special_circular_sequence
for i, j being Element of NAT st i >= 1 & j >= 1 & i + j = len f holds
left_cell (f,i) = right_cell ((Rev f),j)
proof
let f be non constant standard special_circular_sequence; ::_thesis: for i, j being Element of NAT st i >= 1 & j >= 1 & i + j = len f holds
left_cell (f,i) = right_cell ((Rev f),j)
let i, j be Element of NAT ; ::_thesis: ( i >= 1 & j >= 1 & i + j = len f implies left_cell (f,i) = right_cell ((Rev f),j) )
assume that
A1: i >= 1 and
A2: j >= 1 and
A3: i + j = len f ; ::_thesis: left_cell (f,i) = right_cell ((Rev f),j)
A4: i + 1 <= len f by A2, A3, XREAL_1:6;
 len f = len (Rev f) by FINSEQ_5:def_3;
then A5: j + 1 <= len (Rev f) by A1, A3, XREAL_1:6;
A6: GoB (Rev f) = GoB f by Lm1;
now__::_thesis:_for_i1,_j1,_i2,_j2_being_Element_of_NAT_st_[i1,j1]_in_Indices_(GoB_f)_&_[i2,j2]_in_Indices_(GoB_f)_&_f_/._i_=_(GoB_f)_*_(i1,j1)_&_f_/._(i_+_1)_=_(GoB_f)_*_(i2,j2)_&_not_(_i1_=_i2_&_j1_+_1_=_j2_&_right_cell_((Rev_f),j)_=_cell_((GoB_f),(i1_-'_1),j1)_)_&_not_(_i1_+_1_=_i2_&_j1_=_j2_&_right_cell_((Rev_f),j)_=_cell_((GoB_f),i1,j1)_)_&_not_(_i1_=_i2_+_1_&_j1_=_j2_&_right_cell_((Rev_f),j)_=_cell_((GoB_f),i2,(j2_-'_1))_)_holds_
(_i1_=_i2_&_j1_=_j2_+_1_&_right_cell_((Rev_f),j)_=_cell_((GoB_f),i1,j2)_)
let i1, j1, i2, j2 be Element of NAT ; ::_thesis: ( [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. i = (GoB f) * (i1,j1) & f /. (i + 1) = (GoB f) * (i2,j2) & not ( b1 = b3 & b2 + 1 = b4 & right_cell ((Rev f),j) = cell ((GoB f),(b1 -' 1),b2) ) & not ( b1 + 1 = b3 & b2 = b4 & right_cell ((Rev f),j) = cell ((GoB f),b1,b2) ) & not ( b1 = b3 + 1 & b2 = b4 & right_cell ((Rev f),j) = cell ((GoB f),b3,(b4 -' 1)) ) implies ( b1 = b3 & b2 = b4 + 1 & right_cell ((Rev f),j) = cell ((GoB f),b1,b4) ) )
assume that
A7: [i1,j1] in Indices (GoB f) and
A8: [i2,j2] in Indices (GoB f) and
A9: f /. i = (GoB f) * (i1,j1) and
A10: f /. (i + 1) = (GoB f) * (i2,j2) ; ::_thesis: ( ( b1 = b3 & b2 + 1 = b4 & right_cell ((Rev f),j) = cell ((GoB f),(b1 -' 1),b2) ) or ( b1 + 1 = b3 & b2 = b4 & right_cell ((Rev f),j) = cell ((GoB f),b1,b2) ) or ( b1 = b3 + 1 & b2 = b4 & right_cell ((Rev f),j) = cell ((GoB f),b3,(b4 -' 1)) ) or ( b1 = b3 & b2 = b4 + 1 & right_cell ((Rev f),j) = cell ((GoB f),b1,b4) ) )
 1 <= i + 1 by NAT_1:11;
then A11: i + 1 in dom f by A4, FINSEQ_3:25;
 (i + 1) + j = (len f) + 1 by A3;
then A12: (Rev f) /. j = (GoB f) * (i2,j2) by A10, A11, FINSEQ_5:66;
 i <= len f by A4, NAT_1:13;
then A13: i in dom f by A1, FINSEQ_3:25;
 (j + 1) + i = (len f) + 1 by A3;
then A14: (Rev f) /. (j + 1) = (GoB f) * (i1,j1) by A9, A13, FINSEQ_5:66;
 1 <= i1 by A7, MATRIX_1:38;
then A15: (i1 -' 1) + 1 = i1 by XREAL_1:235;
 1 <= j1 by A7, MATRIX_1:38;
then A16: (j1 -' 1) + 1 = j1 by XREAL_1:235;
reconsider i19 = i1, i29 = i2, j19 = j1, j29 = j2 as Element of REAL ;
 f is_sequence_on GoB f by GOBOARD5:def_5;
then  (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A7, A8, A9, A10, A11, A13, GOBOARD1:def_9;
then A17: ( ( abs (i19 - i29) = 1 & j1 = j2 ) or ( abs (j19 - j29) = 1 & i1 = i2 ) ) by SEQM_3:42;
percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A17, SEQM_3:41;
case ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: right_cell ((Rev f),j) = cell ((GoB f),(i1 -' 1),j1)
hence  right_cell ((Rev f),j) = cell ((GoB f),(i1 -' 1),j1) by A2, A5, A6, A7, A8, A12, A14, A15, GOBOARD5:30; ::_thesis: verum
end;
case ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: right_cell ((Rev f),j) = cell ((GoB f),i1,j1)
hence  right_cell ((Rev f),j) = cell ((GoB f),i1,j1) by A2, A5, A6, A7, A8, A12, A14, A16, GOBOARD5:29; ::_thesis: verum
end;
case ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: right_cell ((Rev f),j) = cell ((GoB f),i2,(j2 -' 1))
hence  right_cell ((Rev f),j) = cell ((GoB f),i2,(j2 -' 1)) by A2, A5, A6, A7, A8, A12, A14, A16, GOBOARD5:28; ::_thesis: verum
end;
case ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: right_cell ((Rev f),j) = cell ((GoB f),i1,j2)
hence  right_cell ((Rev f),j) = cell ((GoB f),i1,j2) by A2, A5, A6, A7, A8, A12, A14, A15, GOBOARD5:27; ::_thesis: verum
end;
end;
end;
hence  left_cell (f,i) = right_cell ((Rev f),j) by A1, A4, GOBOARD5:def_7; ::_thesis: verum
end;

theorem Th10: :: GOBOARD9:10
for f being non constant standard special_circular_sequence
for i, j being Element of NAT st i >= 1 & j >= 1 & i + j = len f holds
left_cell ((Rev f),i) = right_cell (f,j)
proof
let f be non constant standard special_circular_sequence; ::_thesis: for i, j being Element of NAT st i >= 1 & j >= 1 & i + j = len f holds
left_cell ((Rev f),i) = right_cell (f,j)
let i, j be Element of NAT ; ::_thesis: ( i >= 1 & j >= 1 & i + j = len f implies left_cell ((Rev f),i) = right_cell (f,j) )
A1: len (Rev f) = len f by FINSEQ_5:def_3;
 Rev (Rev f) = f ;
hence  ( i >= 1 & j >= 1 & i + j = len f implies left_cell ((Rev f),i) = right_cell (f,j) ) by A1, Th9; ::_thesis: verum
end;

theorem Th11: :: GOBOARD9:11
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )
proof
let f be non constant standard special_circular_sequence; ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds
ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) )
assume that
A1: 1 <= k and
A2: k + 1 <= len f ; ::_thesis: ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )
A3: f is_sequence_on GoB f by GOBOARD5:def_5;
 k <= len f by A2, NAT_1:13;
then A4: k in dom f by A1, FINSEQ_3:25;
then consider i1, j1 being Element of NAT  such that
A5: [i1,j1] in Indices (GoB f) and
A6: f /. k = (GoB f) * (i1,j1) by A3, GOBOARD1:def_9;
 1 <= k + 1 by NAT_1:11;
then A7: k + 1 in dom f by A2, FINSEQ_3:25;
then consider i2, j2 being Element of NAT  such that
A8: [i2,j2] in Indices (GoB f) and
A9: f /. (k + 1) = (GoB f) * (i2,j2) by A3, GOBOARD1:def_9;
 1 <= i1 by A5, MATRIX_1:38;
then A10: (i1 -' 1) + 1 = i1 by XREAL_1:235;
 1 <= j1 by A5, MATRIX_1:38;
then A11: (j1 -' 1) + 1 = j1 by XREAL_1:235;
reconsider i19 = i1, i29 = i2, j19 = j1, j29 = j2 as Element of REAL ;
 (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A3, A4, A5, A6, A7, A8, A9, GOBOARD1:def_9;
then A12: ( ( abs (i19 - i29) = 1 & j1 = j2 ) or ( abs (j19 - j29) = 1 & i1 = i2 ) ) by SEQM_3:42;
A13: i1 <= len (GoB f) by A5, MATRIX_1:38;
A14: j1 <= width (GoB f) by A5, MATRIX_1:38;
percases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A12, SEQM_3:41;
supposeA15: ( i1 = i2 & j1 + 1 = j2 ) ; ::_thesis: ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )
take  i1 -' 1 ; ::_thesis: ex j being Element of NAT st
( i1 -' 1 <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),(i1 -' 1),j) = left_cell (f,k) )
take  j1 ; ::_thesis: ( i1 -' 1 <= len (GoB f) & j1 <= width (GoB f) & cell ((GoB f),(i1 -' 1),j1) = left_cell (f,k) )
 i1 -' 1 <= i1 by NAT_D:35;
hence  i1 -' 1 <= len (GoB f) by A13, XXREAL_0:2; ::_thesis: ( j1 <= width (GoB f) & cell ((GoB f),(i1 -' 1),j1) = left_cell (f,k) )
thus  j1 <= width (GoB f) by A5, MATRIX_1:38; ::_thesis: cell ((GoB f),(i1 -' 1),j1) = left_cell (f,k)
thus  cell ((GoB f),(i1 -' 1),j1) = left_cell (f,k) by A1, A2, A5, A6, A8, A9, A10, A15, GOBOARD5:27; ::_thesis: verum
end;
supposeA16: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )
take  i1 ; ::_thesis: ex j being Element of NAT st
( i1 <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i1,j) = left_cell (f,k) )
take  j1 ; ::_thesis: ( i1 <= len (GoB f) & j1 <= width (GoB f) & cell ((GoB f),i1,j1) = left_cell (f,k) )
thus  i1 <= len (GoB f) by A5, MATRIX_1:38; ::_thesis: ( j1 <= width (GoB f) & cell ((GoB f),i1,j1) = left_cell (f,k) )
thus  j1 <= width (GoB f) by A5, MATRIX_1:38; ::_thesis: cell ((GoB f),i1,j1) = left_cell (f,k)
thus  cell ((GoB f),i1,j1) = left_cell (f,k) by A1, A2, A5, A6, A8, A9, A11, A16, GOBOARD5:28; ::_thesis: verum
end;
supposeA17: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )
take  i2 ; ::_thesis: ex j being Element of NAT st
( i2 <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i2,j) = left_cell (f,k) )
take  j1 -' 1 ; ::_thesis: ( i2 <= len (GoB f) & j1 -' 1 <= width (GoB f) & cell ((GoB f),i2,(j1 -' 1)) = left_cell (f,k) )
thus  i2 <= len (GoB f) by A8, MATRIX_1:38; ::_thesis: ( j1 -' 1 <= width (GoB f) & cell ((GoB f),i2,(j1 -' 1)) = left_cell (f,k) )
 j1 -' 1 <= j1 by NAT_D:35;
hence  j1 -' 1 <= width (GoB f) by A14, XXREAL_0:2; ::_thesis: cell ((GoB f),i2,(j1 -' 1)) = left_cell (f,k)
thus  cell ((GoB f),i2,(j1 -' 1)) = left_cell (f,k) by A1, A2, A5, A6, A8, A9, A11, A17, GOBOARD5:29; ::_thesis: verum
end;
supposeA18: ( i1 = i2 & j1 = j2 + 1 ) ; ::_thesis: ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) )
take  i1 ; ::_thesis: ex j being Element of NAT st
( i1 <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i1,j) = left_cell (f,k) )
take  j2 ; ::_thesis: ( i1 <= len (GoB f) & j2 <= width (GoB f) & cell ((GoB f),i1,j2) = left_cell (f,k) )
thus  i1 <= len (GoB f) by A5, MATRIX_1:38; ::_thesis: ( j2 <= width (GoB f) & cell ((GoB f),i1,j2) = left_cell (f,k) )
thus  j2 <= width (GoB f) by A8, MATRIX_1:38; ::_thesis: cell ((GoB f),i1,j2) = left_cell (f,k)
thus  cell ((GoB f),i1,j2) = left_cell (f,k) by A1, A2, A5, A6, A8, A9, A10, A18, GOBOARD5:30; ::_thesis: verum
end;
end;
end;

theorem Th12: :: GOBOARD9:12
for j being Element of NAT
for G being Go-board st j <= width G holds
Int (h_strip (G,j)) is convex
proof
let j be Element of NAT ; ::_thesis: for G being Go-board st j <= width G holds
Int (h_strip (G,j)) is convex
let G be Go-board; ::_thesis: ( j <= width G implies Int (h_strip (G,j)) is convex )
assume A1: j <= width G ; ::_thesis: Int (h_strip (G,j)) is convex
percases ( j = 0 or j = width G or ( 1 <= j & j < width G ) ) by A1, NAT_1:14, XXREAL_0:1;
suppose j = 0 ; ::_thesis: Int (h_strip (G,j)) is convex
then  Int (h_strip (G,j)) =  {  |[r,s]| where r, s is Real : s < (G * (1,1)) `2  }  by GOBOARD6:15;
hence  Int (h_strip (G,j)) is convex by JORDAN1:17; ::_thesis: verum
end;
suppose j = width G ; ::_thesis: Int (h_strip (G,j)) is convex
then  Int (h_strip (G,j)) =  {  |[r,s]| where r, s is Real : (G * (1,(width G))) `2 < s  }  by GOBOARD6:16;
hence  Int (h_strip (G,j)) is convex by JORDAN1:15; ::_thesis: verum
end;
suppose ( 1 <= j & j < width G ) ; ::_thesis: Int (h_strip (G,j)) is convex
then A2: Int (h_strip (G,j)) =  {  |[r,s]| where r, s is Real : ( (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 )  }  by GOBOARD6:17;
A3:  {  |[r,s]| where r, s is Real : (G * (1,j)) `2 < s  }  c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  |[r,s]| where r, s is Real : (G * (1,j)) `2 < s  }  or x in the carrier of (TOP-REAL 2) )
assume  x in  {  |[r,s]| where r, s is Real : (G * (1,j)) `2 < s  }  ; ::_thesis: x in the carrier of (TOP-REAL 2)
then  ex r, s being Real st
( x = |[r,s]| & (G * (1,j)) `2 < s ) ;
hence  x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
  {  |[r,s]| where r, s is Real : s < (G * (1,(j + 1))) `2  }  c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  |[r,s]| where r, s is Real : s < (G * (1,(j + 1))) `2  }  or x in the carrier of (TOP-REAL 2) )
assume  x in  {  |[r,s]| where r, s is Real : s < (G * (1,(j + 1))) `2  }  ; ::_thesis: x in the carrier of (TOP-REAL 2)
then  ex r, s being Real st
( x = |[r,s]| & s < (G * (1,(j + 1))) `2 ) ;
hence  x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
then reconsider P =  {  |[r,s]| where r, s is Real : (G * (1,j)) `2 < s  }  , Q =  {  |[r,s]| where r, s is Real : s < (G * (1,(j + 1))) `2  }  as Subset of (TOP-REAL 2) by A3;
A4: Int (h_strip (G,j)) = P /\ Q
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: P /\ Q c= Int (h_strip (G,j))
let x be set ; ::_thesis: ( x in Int (h_strip (G,j)) implies x in P /\ Q )
assume  x in Int (h_strip (G,j)) ; ::_thesis: x in P /\ Q
then A5: ex r, s being Real st
( x = |[r,s]| & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) by A2;
then A6: x in P ;
 x in Q by A5;
hence  x in P /\ Q by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P /\ Q or x in Int (h_strip (G,j)) )
assume A7: x in P /\ Q ; ::_thesis: x in Int (h_strip (G,j))
then  x in P by XBOOLE_0:def_4;
then consider r1, s1 being Real such that
A8: x = |[r1,s1]| and
A9: (G * (1,j)) `2 < s1 ;
 x in Q by A7, XBOOLE_0:def_4;
then consider r2, s2 being Real such that
A10: x = |[r2,s2]| and
A11: s2 < (G * (1,(j + 1))) `2 ;
 s1 = s2 by A8, A10, SPPOL_2:1;
hence  x in Int (h_strip (G,j)) by A2, A8, A9, A11; ::_thesis: verum
end;
A12: P is convex by JORDAN1:15;
 Q is convex by JORDAN1:17;
hence  Int (h_strip (G,j)) is convex by A4, A12, Th6; ::_thesis: verum
end;
end;
end;

theorem Th13: :: GOBOARD9:13
for i being Element of NAT
for G being Go-board st i <= len G holds
Int (v_strip (G,i)) is convex
proof
let i be Element of NAT ; ::_thesis: for G being Go-board st i <= len G holds
Int (v_strip (G,i)) is convex
let G be Go-board; ::_thesis: ( i <= len G implies Int (v_strip (G,i)) is convex )
assume A1: i <= len G ; ::_thesis: Int (v_strip (G,i)) is convex
percases ( i = 0 or i = len G or ( 1 <= i & i < len G ) ) by A1, NAT_1:14, XXREAL_0:1;
suppose i = 0 ; ::_thesis: Int (v_strip (G,i)) is convex
then  Int (v_strip (G,i)) =  {  |[r,s]| where r, s is Real : r < (G * (1,1)) `1  }  by GOBOARD6:12;
hence  Int (v_strip (G,i)) is convex by JORDAN1:13; ::_thesis: verum
end;
suppose i = len G ; ::_thesis: Int (v_strip (G,i)) is convex
then  Int (v_strip (G,i)) =  {  |[r,s]| where r, s is Real : (G * ((len G),1)) `1 < r  }  by GOBOARD6:13;
hence  Int (v_strip (G,i)) is convex by JORDAN1:11; ::_thesis: verum
end;
suppose ( 1 <= i & i < len G ) ; ::_thesis: Int (v_strip (G,i)) is convex
then A2: Int (v_strip (G,i)) =  {  |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 )  }  by GOBOARD6:14;
A3:  {  |[r,s]| where r, s is Real : (G * (i,1)) `1 < r  }  c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  |[r,s]| where r, s is Real : (G * (i,1)) `1 < r  }  or x in the carrier of (TOP-REAL 2) )
assume  x in  {  |[r,s]| where r, s is Real : (G * (i,1)) `1 < r  }  ; ::_thesis: x in the carrier of (TOP-REAL 2)
then  ex r, s being Real st
( x = |[r,s]| & (G * (i,1)) `1 < r ) ;
hence  x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
  {  |[r,s]| where r, s is Real : r < (G * ((i + 1),1)) `1  }  c= the carrier of (TOP-REAL 2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  |[r,s]| where r, s is Real : r < (G * ((i + 1),1)) `1  }  or x in the carrier of (TOP-REAL 2) )
assume  x in  {  |[r,s]| where r, s is Real : r < (G * ((i + 1),1)) `1  }  ; ::_thesis: x in the carrier of (TOP-REAL 2)
then  ex r, s being Real st
( x = |[r,s]| & r < (G * ((i + 1),1)) `1 ) ;
hence  x in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
then reconsider P =  {  |[r,s]| where r, s is Real : (G * (i,1)) `1 < r  }  , Q =  {  |[r,s]| where r, s is Real : r < (G * ((i + 1),1)) `1  }  as Subset of (TOP-REAL 2) by A3;
A4: Int (v_strip (G,i)) = P /\ Q
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: P /\ Q c= Int (v_strip (G,i))
let x be set ; ::_thesis: ( x in Int (v_strip (G,i)) implies x in P /\ Q )
assume  x in Int (v_strip (G,i)) ; ::_thesis: x in P /\ Q
then A5: ex r, s being Real st
( x = |[r,s]| & (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 ) by A2;
then A6: x in P ;
 x in Q by A5;
hence  x in P /\ Q by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P /\ Q or x in Int (v_strip (G,i)) )
assume A7: x in P /\ Q ; ::_thesis: x in Int (v_strip (G,i))
then  x in P by XBOOLE_0:def_4;
then consider r1, s1 being Real such that
A8: x = |[r1,s1]| and
A9: (G * (i,1)) `1 < r1 ;
 x in Q by A7, XBOOLE_0:def_4;
then consider r2, s2 being Real such that
A10: x = |[r2,s2]| and
A11: r2 < (G * ((i + 1),1)) `1 ;
 r1 = r2 by A8, A10, SPPOL_2:1;
hence  x in Int (v_strip (G,i)) by A2, A8, A9, A11; ::_thesis: verum
end;
A12: P is convex by JORDAN1:11;
 Q is convex by JORDAN1:13;
hence  Int (v_strip (G,i)) is convex by A4, A12, Th6; ::_thesis: verum
end;
end;
end;

theorem Th14: :: GOBOARD9:14
for i, j being Element of NAT
for G being Go-board st i <= len G & j <= width G holds
Int (cell (G,i,j)) <> {}
proof
let i, j be Element of NAT ; ::_thesis: for G being Go-board st i <= len G & j <= width G holds
Int (cell (G,i,j)) <> {}
let G be Go-board; ::_thesis: ( i <= len G & j <= width G implies Int (cell (G,i,j)) <> {} )
assume that
A1: i <= len G and
A2: j <= width G ; ::_thesis: Int (cell (G,i,j)) <> {}
A3: ( j = width G or j < width G ) by A2, XXREAL_0:1;
A4: ( i = len G or i < len G ) by A1, XXREAL_0:1;
set p = the Point of (TOP-REAL 2);
percases ( ( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G ) or ( 1 <= i & i + 1 <= len G & j = width G ) or ( 1 <= i & i + 1 <= len G & j = 0 ) or ( 1 <= j & j + 1 <= width G & i = 0 ) or ( 1 <= j & j + 1 <= width G & i = len G ) or ( i = 0 & j = 0 ) or ( i = len G & j = width G ) or ( i = 0 & j = width G ) or ( i = len G & j = 0 ) ) by A3, A4, NAT_1:13, NAT_1:14;
suppose ( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G ) ; ::_thesis: Int (cell (G,i,j)) <> {}
then  LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))), the Point of (TOP-REAL 2)) meets Int (cell (G,i,j)) by GOBOARD6:82;
hence  Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum
end;
suppose ( 1 <= i & i + 1 <= len G & j = width G ) ; ::_thesis: Int (cell (G,i,j)) <> {}
then  LSeg ( the Point of (TOP-REAL 2),(((1 / 2) * ((G * (i,j)) + (G * ((i + 1),j)))) + |[0,1]|)) meets Int (cell (G,i,j)) by GOBOARD6:83;
hence  Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum
end;
suppose ( 1 <= i & i + 1 <= len G & j = 0 ) ; ::_thesis: Int (cell (G,i,j)) <> {}
then  LSeg ((((1 / 2) * ((G * (i,(j + 1))) + (G * ((i + 1),(j + 1))))) - |[0,1]|), the Point of (TOP-REAL 2)) meets Int (cell (G,i,j)) by GOBOARD6:84;
hence  Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum
end;
suppose ( 1 <= j & j + 1 <= width G & i = 0 ) ; ::_thesis: Int (cell (G,i,j)) <> {}
then  LSeg ((((1 / 2) * ((G * ((i + 1),j)) + (G * ((i + 1),(j + 1))))) - |[1,0]|), the Point of (TOP-REAL 2)) meets Int (cell (G,i,j)) by GOBOARD6:85;
hence  Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum
end;
suppose ( 1 <= j & j + 1 <= width G & i = len G ) ; ::_thesis: Int (cell (G,i,j)) <> {}
then  LSeg ( the Point of (TOP-REAL 2),(((1 / 2) * ((G * (i,j)) + (G * (i,(j + 1))))) + |[1,0]|)) meets Int (cell (G,i,j)) by GOBOARD6:86;
hence  Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum
end;
suppose ( i = 0 & j = 0 ) ; ::_thesis: Int (cell (G,i,j)) <> {}
then  LSeg ( the Point of (TOP-REAL 2),((G * ((i + 1),(j + 1))) - |[1,1]|)) meets Int (cell (G,i,j)) by GOBOARD6:87;
hence  Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum
end;
suppose ( i = len G & j = width G ) ; ::_thesis: Int (cell (G,i,j)) <> {}
then  LSeg ( the Point of (TOP-REAL 2),((G * (i,j)) + |[1,1]|)) meets Int (cell (G,i,j)) by GOBOARD6:88;
hence  Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum
end;
suppose ( i = 0 & j = width G ) ; ::_thesis: Int (cell (G,i,j)) <> {}
then  LSeg ( the Point of (TOP-REAL 2),((G * ((i + 1),j)) + |[(- 1),1]|)) meets Int (cell (G,i,j)) by GOBOARD6:89;
hence  Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum
end;
suppose ( i = len G & j = 0 ) ; ::_thesis: Int (cell (G,i,j)) <> {}
then  LSeg ( the Point of (TOP-REAL 2),((G * (i,(j + 1))) + |[1,(- 1)]|)) meets Int (cell (G,i,j)) by GOBOARD6:90;
hence  Int (cell (G,i,j)) <> {} by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;

theorem Th15: :: GOBOARD9:15
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
Int (left_cell (f,k)) <> {}
proof
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)) <> {}
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies Int (left_cell (f,k)) <> {} )
assume that
A1: 1 <= k and
A2: k + 1 <= len f ; ::_thesis: Int (left_cell (f,k)) <> {}
 ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) by A1, A2, Th11;
hence  Int (left_cell (f,k)) <> {} by Th14; ::_thesis: verum
end;

theorem Th16: :: GOBOARD9:16
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
Int (right_cell (f,k)) <> {}
proof
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 (right_cell (f,k)) <> {}
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies Int (right_cell (f,k)) <> {} )
assume that
A1: 1 <= k and
A2: k + 1 <= len f ; ::_thesis: Int (right_cell (f,k)) <> {}
A3: len f = len (Rev f) by FINSEQ_5:def_3;
 k <= len f by A2, NAT_1:13;
then A4: ((len f) -' k) + k = len f by XREAL_1:235;
then A5: ((len f) -' k) + 1 <= len f by A1, XREAL_1:6;
A6: (len f) -' k >= 1 by A2, A4, XREAL_1:6;
then  right_cell (f,k) = left_cell ((Rev f),((len f) -' k)) by A1, A4, Th10;
hence  Int (right_cell (f,k)) <> {} by A3, A5, A6, Th15; ::_thesis: verum
end;

theorem Th17: :: GOBOARD9:17
for i, j being Element of NAT
for G being Go-board st i <= len G & j <= width G holds
Int (cell (G,i,j)) is convex
proof
let i, j be Element of NAT ; ::_thesis: for G being Go-board st i <= len G & j <= width G holds
Int (cell (G,i,j)) is convex
let G be Go-board; ::_thesis: ( i <= len G & j <= width G implies Int (cell (G,i,j)) is convex )
assume that
A1: i <= len G and
A2: j <= width G ; ::_thesis: Int (cell (G,i,j)) is convex
set P = Int (cell (G,i,j));
A3: Int (cell (G,i,j)) = (Int (v_strip (G,i))) /\ (Int (h_strip (G,j))) by TOPS_1:17;
A4: Int (v_strip (G,i)) is convex by A1, Th13;
 Int (h_strip (G,j)) is convex by A2, Th12;
hence  Int (cell (G,i,j)) is convex by A3, A4, Th6; ::_thesis: verum
end;

theorem :: GOBOARD9:18
canceled;

theorem Th19: :: GOBOARD9:19
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
Int (left_cell (f,k)) is convex
proof
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)) is convex
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies Int (left_cell (f,k)) is convex )
assume that
A1: 1 <= k and
A2: k + 1 <= len f ; ::_thesis: Int (left_cell (f,k)) is convex
 ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) by A1, A2, Th11;
hence  Int (left_cell (f,k)) is convex by Th17; ::_thesis: verum
end;

theorem Th20: :: GOBOARD9:20
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
Int (right_cell (f,k)) is convex
proof
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 (right_cell (f,k)) is convex
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies Int (right_cell (f,k)) is convex )
assume that
A1: 1 <= k and
A2: k + 1 <= len f ; ::_thesis: Int (right_cell (f,k)) is convex
A3: len f = len (Rev f) by FINSEQ_5:def_3;
 k <= len f by A2, NAT_1:13;
then A4: ((len f) -' k) + k = len f by XREAL_1:235;
then A5: ((len f) -' k) + 1 <= len f by A1, XREAL_1:6;
A6: (len f) -' k >= 1 by A2, A4, XREAL_1:6;
then  right_cell (f,k) = left_cell ((Rev f),((len f) -' k)) by A1, A4, Th10;
hence  Int (right_cell (f,k)) is convex by A3, A5, A6, Th19; ::_thesis: verum
end;

definition
let f be non constant standard special_circular_sequence;
A1: 1 + 1 < len f by GOBOARD7:34, XXREAL_0:2;
then A2: Int (left_cell (f,1)) <> {} by Th15;
A3: Int (right_cell (f,1)) <> {} by A1, Th16;
func LeftComp f ->  Subset of (TOP-REAL 2) means :Def1: :: GOBOARD9:def 1
( it is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= it );
existence
 ex b1 being Subset of (TOP-REAL 2) st
( b1 is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b1 )
proof
A4: Int (left_cell (f,1)) is convex by A1, Th19;
 Int (left_cell (f,1)) misses L~ f by A1, GOBOARD8:37;
then A5: Int (left_cell (f,1)) c= (L~ f) ` by SUBSET_1:23;
then  (L~ f) ` <> {} by A1, Th15, XBOOLE_1:3;
hence  ex b1 being Subset of (TOP-REAL 2) st
( b1 is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b1 ) by A2, A4, A5, Th3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of (TOP-REAL 2) st b1 is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b1 & b2 is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b2 holds
b1 = b2 by A2, Th1, XBOOLE_1:67;
func RightComp f ->  Subset of (TOP-REAL 2) means :Def2: :: GOBOARD9:def 2
( it is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= it );
existence
 ex b1 being Subset of (TOP-REAL 2) st
( b1 is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b1 )
proof
A6: Int (right_cell (f,1)) is convex by A1, Th20;
 Int (right_cell (f,1)) misses L~ f by A1, GOBOARD8:38;
then A7: Int (right_cell (f,1)) c= (L~ f) ` by SUBSET_1:23;
then  (L~ f) ` <> {} by A1, Th16, XBOOLE_1:3;
hence  ex b1 being Subset of (TOP-REAL 2) st
( b1 is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b1 ) by A3, A6, A7, Th3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of (TOP-REAL 2) st b1 is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b1 & b2 is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b2 holds
b1 = b2 by A3, Th1, XBOOLE_1:67;
end;

:: deftheorem Def1 defines LeftComp GOBOARD9:def_1_:_
 for f being non constant standard special_circular_sequence
for b2 being Subset of (TOP-REAL 2) holds
( b2 = LeftComp f iff ( b2 is_a_component_of (L~ f) ` & Int (left_cell (f,1)) c= b2 ) );

:: deftheorem Def2 defines RightComp GOBOARD9:def_2_:_
 for f being non constant standard special_circular_sequence
for b2 being Subset of (TOP-REAL 2) holds
( b2 = RightComp f iff ( b2 is_a_component_of (L~ f) ` & Int (right_cell (f,1)) c= b2 ) );

theorem Th21: :: GOBOARD9:21
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
Int (left_cell (f,k)) c= LeftComp f
proof
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 S1[ Element of NAT ] means ( 1 <= $1 & $1 + 1 <= len f implies Int (left_cell (f,$1)) c= LeftComp f );
A1: S1[ 0 ] ;
A2: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
thus  S1[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
percases ( 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;
supposeA6: 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__::_thesis:_(_i0_=_i2_implies_not_j0_=_j2_)
assume that
A40: i0 = i2 and
A41: j0 = j2 ; ::_thesis: contradiction
A42: now__::_thesis:_(_k_<=_1_implies_not_(k_+_1)_+_1_>=_len_f_)
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;
percases ( 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__::_thesis:_Int_(left_cell_(f,(k_+_1)))_c=_LeftComp_f
percases ( ( 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;
supposethat 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]|)) 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 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]|)) c= LeftComp f by A3, A5, A6, A55, A60, A62, Th4, NAT_1:13;
A64: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A61, A63, A21, A22, A58, GOBOARD6:84, Th4, A64; ::_thesis: verum
end;
supposethat A65: i0 = i1 + 1 and
A66: i1 = i2 + 1 and
A67: j0 <> 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A68: left_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) by A6, A7, A10, A11, A13, A14, A30, A46, A65, GOBOARD5:29;
 1 < j0 by A24, A67, XXREAL_0:1;
then A69: 1 <= j0 -' 1 by A30, A46, A65, NAT_1:13;
A70: left_cell (f,(k + 1)) = cell ((GoB f),i2,(j1 -' 1)) by A4, A5, A13, A14, A16, A17, A31, A46, A66, GOBOARD5:29;
A71: 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, A65, A69, 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, A65, A66, A69, 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 A72: 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, A68, A71, Th4, NAT_1:13;
A73: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A30, A55, A65, A66, A70, A72, A21, A22, A25, A46, A69, GOBOARD6:82, Th4, A73; ::_thesis: verum
end;
supposethat A74: i0 = i1 + 1 and
A75: 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, A74, A75, GOBOARD5:29
.= left_cell (f,(k + 1)) by A4, A5, A13, A14, A16, A17, A31, A45, A75, GOBOARD5:30 ;
hence  Int (left_cell (f,(k + 1))) c= LeftComp f by A3, A5, A6, NAT_1:13; ::_thesis: verum
end;
supposethat A76: j0 = j1 + 1 and
A77: i1 = i2 + 1 and
A78: i0 = len (GoB f) and
A79: j1 = 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A80: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A45, A76, GOBOARD5:30;
A81: 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, A76, A78, A79, 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 A82: 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, A80, A81, Th4, NAT_1:13;
A83: Int (cell ((GoB f),i1,0)) is convex by A21, A26, A27, Th17;
 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 A84: Int (cell ((GoB f),i1,0)) c= LeftComp f by A55, A82, A30, A76, A78, GOBOARD6:90, Th4, A83;
A85: left_cell (f,(k + 1)) = cell ((GoB f),i2,0) by A4, A5, A13, A14, A16, A17, A31, A46, A77, A79, GOBOARD5:29;
A86: 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, A76, A78, 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 A87: 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, A84, A86, Th4;
A88: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A85, A87, A22, A30, A45, A76, A77, A78, GOBOARD6:84, Th4, A88; ::_thesis: verum
end;
supposethat A89: j0 = j1 + 1 and
A90: i1 = i2 + 1 and
A91: i0 <> len (GoB f) and
A92: j1 = 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A93: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A45, A89, GOBOARD5:30;
 len (GoB f) > i0 by A19, A91, XXREAL_0:1;
then A94: len (GoB f) >= i0 + 1 by NAT_1:13;
A95: 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, A89, A92, A94, 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, A89, A90, A92, A94, 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 A96: 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, A93, A95, Th4, NAT_1:13;
A97: Int (cell ((GoB f),i1,0)) is convex by A21, A26, A27, Th17;
 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 A98: Int (cell ((GoB f),i1,0)) c= LeftComp f by A55, A96, A20, A30, A89, A94, GOBOARD6:84, Th4, A97;
A99: left_cell (f,(k + 1)) = cell ((GoB f),i2,0) by A4, A5, A13, A14, A16, A17, A31, A46, A90, A92, GOBOARD5:29;
A100: 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, A89, A90, A94, 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, A89, A90, A94, 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 A101: 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, A98, A100, Th4;
A102: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A99, A101, A21, A22, A90, GOBOARD6:84, Th4, A102; ::_thesis: verum
end;
supposethat A103: j0 = j1 + 1 and
A104: i1 = i2 + 1 and
A105: i0 = len (GoB f) and
A106: j1 <> 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A107: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A45, A103, GOBOARD5:30;
 1 < j1 by A26, A106, XXREAL_0:1;
then A108: 1 <= j1 -' 1 by A46, NAT_1:13;
A109: j1 + 1 = (j1 -' 1) + (1 + 1) by A46;
A110: 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, A103, A105, 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, A103, A108, A109, 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 A111: 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, A107, A110, Th4, NAT_1:13;
 j1 > 1 by A26, A106, XXREAL_0:1;
then A112: 1 <= j1 -' 1 by A46, NAT_1:13;
A113: Int (cell ((GoB f),i1,(j1 -' 1))) is convex by A21, A47, Th17;
 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 A114: Int (cell ((GoB f),i1,(j1 -' 1))) c= LeftComp f by A55, A111, A27, A30, A46, A103, A105, GOBOARD6:86, Th4, A113, A112;
A115: left_cell (f,(k + 1)) = cell ((GoB f),i2,(j1 -' 1)) by A4, A5, A13, A14, A16, A17, A31, A46, A104, GOBOARD5:29;
A116: 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, A103, A105, A108, GOBOARD6:86;
A117: i1 -' 1 = i2 by A104, 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, A103, A104, A105, A108, A109, 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 A118: 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, A114, A116, Th4;
A119: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A115, A118, A21, A22, A27, A46, A104, A108, A117, GOBOARD6:82, Th4, A119; ::_thesis: verum
end;
supposethat A120: j0 = j1 + 1 and
A121: i1 = i2 + 1 and
A122: i0 <> len (GoB f) and
A123: j1 <> 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A124: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A45, A120, GOBOARD5:30;
 1 < j1 by A26, A123, XXREAL_0:1;
then A125: 1 <= j1 -' 1 by A46, NAT_1:13;
 len (GoB f) > i0 by A19, A122, XXREAL_0:1;
then A126: len (GoB f) >= i0 + 1 by NAT_1:13;
A127: j1 + 1 = (j1 -' 1) + (1 + 1) by A46;
A128: 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, A120, A126, 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, A120, A121, A125, A126, A127, 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 A129: 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, A124, A128, Th4, NAT_1:13;
 j1 > 1 by A26, A123, XXREAL_0:1;
then A130: 1 <= j1 -' 1 by A46, NAT_1:13;
A131: Int (cell ((GoB f),i1,(j1 -' 1))) is convex by A21, A47, Th17;
 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 A132: Int (cell ((GoB f),i1,(j1 -' 1))) c= LeftComp f by A30, A55, A120, A129, A20, A27, A46, A126, GOBOARD6:82, Th4, A131, A130;
A133: left_cell (f,(k + 1)) = cell ((GoB f),i2,(j1 -' 1)) by A4, A5, A13, A14, A16, A17, A31, A46, A121, GOBOARD5:29;
A134: 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, A120, A125, A126, GOBOARD6:82;
 i1 < len (GoB f) by A21, A30, A120, A122, 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, A120, A121, A125, A127, 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 A135: 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, A132, A134, Th4;
A136: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A121, A133, A135, A21, A22, A27, A46, A125, GOBOARD6:82, Th4, A136; ::_thesis: verum
end;
supposethat A137: j0 = j1 + 1 and
A138: j1 = j2 + 1 and
A139: i0 = len (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A140: left_cell (f,k) = cell ((GoB f),(len (GoB f)),j1) by A6, A7, A10, A11, A13, A14, A30, A48, A137, A139, GOBOARD5:30;
A141: left_cell (f,(k + 1)) = cell ((GoB f),(len (GoB f)),j2) by A4, A5, A13, A14, A16, A17, A30, A31, A48, A137, A138, A139, GOBOARD5:30;
A142: 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, A137, A138, 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, A137, A138, 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 A143: 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, A140, A142, Th4, NAT_1:13;
A144: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A141, A143, A27, A28, A138, GOBOARD6:86, Th4, A144; ::_thesis: verum
end;
supposethat A145: j0 = j1 + 1 and
A146: j1 = j2 + 1 and
A147: i0 <> len (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A148: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A45, A145, GOBOARD5:30;
 len (GoB f) > i0 by A19, A147, XXREAL_0:1;
then A149: len (GoB f) >= i0 + 1 by NAT_1:13;
A150: left_cell (f,(k + 1)) = cell ((GoB f),i1,j2) by A4, A5, A13, A14, A16, A17, A31, A45, A146, GOBOARD5:30;
A151: 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, A145, A146, A149, 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, A145, A146, A149, 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 A152: 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, A148, A151, Th4, NAT_1:13;
A153: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A150, A152, A20, A27, A28, A30, A145, A146, A149, GOBOARD6:82, Th4, A153; ::_thesis: verum
end;
supposethat A154: i0 + 1 = i1 and
A155: j1 = j2 + 1 and
A156: i1 = len (GoB f) and
A157: j0 = width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A158: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A46, A154, GOBOARD5:28;
A159: 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, A154, A157, 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, A154, A156, A157, 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 A160: 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, A158, A159, Th4, NAT_1:13;
A161: Int (cell ((GoB f),i1,j1)) is convex by A21, A27, Th17;
 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 A162: Int (cell ((GoB f),i1,j1)) c= LeftComp f by A55, A160, A30, A154, A156, A157, GOBOARD6:88, Th4, A161;
A163: left_cell (f,(k + 1)) = cell ((GoB f),i1,j2) by A4, A5, A13, A14, A16, A17, A31, A45, A155, GOBOARD5:30;
A164: 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, A154, A156, A157, 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, A154, A155, A156, A157, 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 A165: LSeg ((((1 / 2) * (((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1)))) + |[1,0]|),(((GoB f) * (i1,j1)) + |[1,1]|)) c= LeftComp f by A55, A162, A164, Th4;
A166: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A163, A165, A27, A28, A155, A156, GOBOARD6:86, Th4, A166; ::_thesis: verum
end;
supposethat A167: i0 + 1 = i1 and
A168: j1 = j2 + 1 and
A169: i1 <> len (GoB f) and
A170: j0 = width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A171: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A46, A167, GOBOARD5:28;
 len (GoB f) > i1 by A21, A169, XXREAL_0:1;
then A172: i1 + 1 <= len (GoB f) by NAT_1:13;
A173: 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, A167, A170, 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, A167, A170, A172, 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 A174: 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, A171, A173, Th4, NAT_1:13;
A175: Int (cell ((GoB f),i1,j1)) is convex by A21, A27, Th17;
 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 A176: Int (cell ((GoB f),i1,j1)) c= LeftComp f by A55, A174, A20, A30, A167, A170, A172, GOBOARD6:83, Th4, A175;
A177: left_cell (f,(k + 1)) = cell ((GoB f),i1,j2) by A4, A5, A13, A14, A16, A17, A31, A45, A168, GOBOARD5:30;
A178: 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, A167, A170, A172, 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, A167, A168, A170, A172, 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 A179: 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, A176, A178, Th4;
A180: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A177, A179, A20, A28, A30, A167, A168, A170, A172, GOBOARD6:82, Th4, A180; ::_thesis: verum
end;
supposethat A181: i0 + 1 = i1 and
A182: j1 = j2 + 1 and
A183: i1 = len (GoB f) and
A184: j0 <> width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A185: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A46, A181, GOBOARD5:28;
 width (GoB f) > j0 by A25, A184, XXREAL_0:1;
then A186: width (GoB f) >= j0 + 1 by NAT_1:13;
A187: 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, A181, A186, 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, A181, A182, A183, A186, 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 A188: 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, A185, A187, Th4, NAT_1:13;
A189: Int (cell ((GoB f),i1,j1)) is convex by A21, A27, Th17;
 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 A190: Int (cell ((GoB f),i1,j1)) c= LeftComp f by A55, A188, A26, A30, A181, A183, A186, GOBOARD6:86, Th4, A189;
A191: left_cell (f,(k + 1)) = cell ((GoB f),i1,j2) by A4, A5, A13, A14, A16, A17, A31, A45, A182, GOBOARD5:30;
A192: 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, A181, A183, A186, 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, A181, A182, A186, 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 A193: 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, A190, A192, Th4;
A194: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A191, A193, A27, A28, A182, A183, GOBOARD6:86, Th4, A194; ::_thesis: verum
end;
supposethat A195: i0 + 1 = i1 and
A196: j1 = j2 + 1 and
A197: i1 <> len (GoB f) and
A198: j0 <> width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A199: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A46, A195, GOBOARD5:28;
 len (GoB f) > i1 by A21, A197, XXREAL_0:1;
then A200: i1 + 1 <= len (GoB f) by NAT_1:13;
 width (GoB f) > j0 by A25, A198, XXREAL_0:1;
then A201: width (GoB f) >= j0 + 1 by NAT_1:13;
A202: 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, A195, A196, A201, 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, A195, A196, A200, A201, 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 A203: 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, A199, A202, Th4, NAT_1:13;
A204: Int (cell ((GoB f),i1,j1)) is convex by A21, A27, Th17;
 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 A205: Int (cell ((GoB f),i1,j1)) c= LeftComp f by A55, A203, A20, A26, A30, A195, A196, A200, A201, GOBOARD6:82, Th4, A204;
A206: left_cell (f,(k + 1)) = cell ((GoB f),i1,j2) by A4, A5, A13, A14, A16, A17, A31, A45, A196, GOBOARD5:30;
A207: 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, A195, A196, A200, A201, 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, A195, A196, A200, A201, 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 A208: 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, A205, A207, Th4;
A209: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A206, A208, A20, A27, A28, A195, A196, A200, GOBOARD6:82, Th4, A209; ::_thesis: verum
end;
supposethat A210: j0 + 1 = j1 and
A211: 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, A210, A211, GOBOARD5:27
.= left_cell (f,(k + 1)) by A4, A5, A13, A14, A16, A17, A31, A210, A211, GOBOARD5:29 ;
hence  Int (left_cell (f,(k + 1))) c= LeftComp f by A3, A5, A6, NAT_1:13; ::_thesis: verum
end;
supposethat A212: i0 = i1 + 1 and
A213: j1 + 1 = j2 and
A214: i1 = 1 and
A215: j1 = 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A216: left_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) by A6, A7, A10, A11, A13, A14, A30, A46, A212, GOBOARD5:29;
 i1 -' 1 <= i1 by NAT_D:35;
then A217: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2;
A218: j1 -' 1 = 0 by A215, XREAL_1:232;
A219: i1 -' 1 = 0 by A214, XREAL_1:232;
 j1 -' 1 <= j1 by NAT_D:35;
then A220: j1 -' 1 <= width (GoB f) by A27, XXREAL_0:2;
A221: 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, A212, A215, A218, 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 A212, A214, A215, 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 A222: 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, A216, A221, Th4, NAT_1:13;
A223: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) is convex by A217, A220, Th17;
 Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) misses L~ f by A217, A220, GOBOARD7:12;
then  Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= (L~ f) ` by SUBSET_1:23;
then A224: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= LeftComp f by A55, A222, A214, A215, A218, GOBOARD6:87, Th4, A223;
A225: left_cell (f,(k + 1)) = cell ((GoB f),(i1 -' 1),j1) by A4, A5, A13, A14, A16, A17, A31, A45, A213, GOBOARD5:27;
A226: 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 A214, A215, A218, 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 A213, A214, A215, 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 A227: LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2)))) - |[1,0]|)) c= LeftComp f by A55, A224, A226, Th4;
A228: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A225, A227, A26, A29, A213, A214, A219, GOBOARD6:85, Th4, A228; ::_thesis: verum
end;
supposethat A229: i0 = i1 + 1 and
A230: j1 + 1 = j2 and
A231: i1 <> 1 and
A232: j1 = 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A233: left_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) by A6, A7, A10, A11, A13, A14, A30, A46, A229, GOBOARD5:29;
 1 < i1 by A20, A231, XXREAL_0:1;
then A234: 1 <= i1 -' 1 by A45, NAT_1:13;
A235: (i1 -' 1) + (1 + 1) = i0 by A45, A229;
 i1 -' 1 <= i1 by NAT_D:35;
then A236: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2;
A237: j1 -' 1 = 0 by A232, XREAL_1:232;
 j1 -' 1 <= j1 by NAT_D:35;
then A238: j1 -' 1 <= width (GoB f) by A27, XXREAL_0:2;
A239: 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, A229, A237, 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, A234, A235, 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 A240: 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, A233, A239, Th4, NAT_1:13;
A241: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) is convex by A236, A238, Th17;
 Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) misses L~ f by A236, A238, GOBOARD7:12;
then  Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= (L~ f) ` by SUBSET_1:23;
then A242: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= LeftComp f by A55, A240, A21, A45, A234, A237, GOBOARD6:84, Th4, A241;
A243: left_cell (f,(k + 1)) = cell ((GoB f),(i1 -' 1),j1) by A4, A5, A13, A14, A16, A17, A31, A45, A230, GOBOARD5:27;
A244: 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, A234, A237, 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, A230, A232, A234, A235, 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 A245: 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, A242, A244, Th4;
A246: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A243, A245, A21, A29, A45, A230, A232, A234, GOBOARD6:82, Th4, A246; ::_thesis: verum
end;
supposethat A247: i0 = i1 + 1 and
A248: j1 + 1 = j2 and
A249: i1 = 1 and
A250: j1 <> 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A251: left_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) by A6, A7, A10, A11, A13, A14, A30, A46, A247, GOBOARD5:29;
 1 < j0 by A24, A30, A247, A250, XXREAL_0:1;
then A252: 1 <= j0 -' 1 by A30, A46, A247, NAT_1:13;
A253: (j0 -' 1) + (1 + 1) = j2 by A30, A46, A247, A248;
A254: 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, A247, A249, A252, 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, A247, A248, A249, A252, A253, 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 A255: 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, A251, A254, Th4, NAT_1:13;
 i1 -' 1 <= i1 by NAT_D:35;
then A256: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2;
A257: i1 -' 1 = 0 by A249, XREAL_1:232;
 j1 -' 1 <= j1 by NAT_D:35;
then A258: j1 -' 1 <= width (GoB f) by A27, XXREAL_0:2;
A259: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) is convex by A256, A258, Th17;
 Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) misses L~ f by A256, A258, GOBOARD7:12;
then  Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= (L~ f) ` by SUBSET_1:23;
then A260: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= LeftComp f by A30, A55, A247, A255, A27, A46, A252, A257, GOBOARD6:85, Th4, A259;
A261: left_cell (f,(k + 1)) = cell ((GoB f),(i1 -' 1),j1) by A4, A5, A13, A14, A16, A17, A31, A45, A248, GOBOARD5:27;
A262: 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, A247, A252, A257, 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, A247, A248, A252, 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 A263: 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, A260, A262, Th4;
A264: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A261, A263, A26, A29, A46, A248, A257, GOBOARD6:85, Th4, A264; ::_thesis: verum
end;
supposethat A265: i0 = i1 + 1 and
A266: j1 + 1 = j2 and
A267: i1 <> 1 and
A268: j1 <> 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A269: left_cell (f,k) = cell ((GoB f),i1,(j1 -' 1)) by A6, A7, A10, A11, A13, A14, A30, A46, A265, GOBOARD5:29;
 1 < j0 by A24, A30, A265, A268, XXREAL_0:1;
then A270: 1 <= j0 -' 1 by A30, A46, A265, NAT_1:13;
 1 < i1 by A20, A267, XXREAL_0:1;
then A271: 1 <= i1 -' 1 by A45, NAT_1:13;
A272: (i1 -' 1) + (1 + 1) = i0 by A45, A265;
A273: (j0 -' 1) + (1 + 1) = j2 by A30, A46, A265, A266;
A274: 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, A265, A270, 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, A266, A270, A271, A272, A273, 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 A275: 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, A269, A274, Th4, NAT_1:13;
 i1 -' 1 <= i1 by NAT_D:35;
then A276: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2;
 j1 -' 1 <= j1 by NAT_D:35;
then A277: j1 -' 1 <= width (GoB f) by A27, XXREAL_0:2;
A278: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) is convex by A276, A277, Th17;
 Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) misses L~ f by A276, A277, GOBOARD7:12;
then  Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= (L~ f) ` by SUBSET_1:23;
then A279: Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) c= LeftComp f by A30, A55, A265, A275, A21, A27, A45, A46, A270, A271, GOBOARD6:82, Th4, A278;
A280: left_cell (f,(k + 1)) = cell ((GoB f),(i1 -' 1),j1) by A4, A5, A13, A14, A16, A17, A31, A45, A266, GOBOARD5:27;
A281: 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, A265, A270, A271, 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, A266, A270, A271, A272, A273, 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 A282: 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, A279, A281, Th4;
A283: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A280, A282, A21, A26, A29, A45, A266, A271, GOBOARD6:82, Th4, A283; ::_thesis: verum
end;
supposethat A284: j0 = j1 + 1 and
A285: 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, A284, GOBOARD5:30
.= left_cell (f,(k + 1)) by A4, A5, A13, A14, A16, A17, A30, A31, A46, A284, A285, GOBOARD5:28 ;
hence  Int (left_cell (f,(k + 1))) c= LeftComp f by A3, A5, A6, NAT_1:13; ::_thesis: verum
end;
supposethat A286: i0 + 1 = i1 and
A287: i1 + 1 = i2 and
A288: j0 = width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A289: left_cell (f,k) = cell ((GoB f),i0,(width (GoB f))) by A6, A7, A10, A11, A13, A14, A30, A49, A286, A288, GOBOARD5:28;
A290: left_cell (f,(k + 1)) = cell ((GoB f),i1,(width (GoB f))) by A4, A5, A13, A14, A16, A17, A30, A31, A49, A286, A287, A288, GOBOARD5:28;
A291: 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, A286, 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, A286, A287, 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 A292: 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, A289, A291, Th4, NAT_1:13;
A293: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A290, A292, A20, A23, A287, GOBOARD6:83, Th4, A293; ::_thesis: verum
end;
supposethat A294: i0 + 1 = i1 and
A295: i1 + 1 = i2 and
A296: j0 <> width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A297: left_cell (f,k) = cell ((GoB f),i0,j1) by A6, A7, A10, A11, A13, A14, A30, A46, A294, GOBOARD5:28;
 width (GoB f) > j0 by A25, A296, XXREAL_0:1;
then A298: width (GoB f) >= j0 + 1 by NAT_1:13;
A299: left_cell (f,(k + 1)) = cell ((GoB f),i1,j1) by A4, A5, A13, A14, A16, A17, A31, A46, A295, GOBOARD5:28;
A300: 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, A294, A298, 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, A294, A295, A298, 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 A301: 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, A297, A300, Th4, NAT_1:13;
A302: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A299, A301, A20, A23, A24, A30, A294, A295, A298, GOBOARD6:82, Th4, A302; ::_thesis: verum
end;
supposethat A303: i0 + 1 = i1 and
A304: 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, A303, GOBOARD5:28
.= left_cell (f,(k + 1)) by A4, A5, A13, A14, A16, A17, A31, A303, A304, GOBOARD5:27 ;
hence  Int (left_cell (f,(k + 1))) c= LeftComp f by A3, A5, A6, NAT_1:13; ::_thesis: verum
end;
supposethat A305: j0 + 1 = j1 and
A306: i1 + 1 = i2 and
A307: i0 = 1 and
A308: j1 = width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A309: left_cell (f,k) = cell ((GoB f),(i1 -' 1),j0) by A6, A7, A10, A11, A13, A14, A30, A45, A305, GOBOARD5:27;
A310: i0 -' 1 = 0 by A307, XREAL_1:232;
A311: j1 -' 1 = j0 by A305, NAT_D:34;
A312: 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, A305, A310, 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 A308, A311, 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 A313: 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, A309, A312, Th4, NAT_1:13;
 i1 -' 1 <= i1 by NAT_D:35;
then A314: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2;
A315: Int (cell ((GoB f),(i1 -' 1),j1)) is convex by A27, A314, Th17;
 Int (cell ((GoB f),(i1 -' 1),j1)) misses L~ f by A27, A314, GOBOARD7:12;
then  Int (cell ((GoB f),(i1 -' 1),j1)) c= (L~ f) ` by SUBSET_1:23;
then A316: Int (cell ((GoB f),(i1 -' 1),j1)) c= LeftComp f by A30, A55, A305, A313, A308, A310, GOBOARD6:89, Th4, A315;
A317: left_cell (f,(k + 1)) = cell ((GoB f),i1,j1) by A4, A5, A13, A14, A16, A17, A31, A305, A306, GOBOARD5:28;
A318: 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, A305, A308, A310, 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 A308, 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 A319: LSeg ((((GoB f) * (1,j1)) + |[(- 1),1]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (2,j1)))) + |[0,1]|)) c= LeftComp f by A55, A316, A318, Th4;
A320: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A317, A319, A23, A30, A305, A306, A307, A308, GOBOARD6:83, Th4, A320; ::_thesis: verum
end;
supposethat 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;
 1 < i0 by A18, A323, XXREAL_0:1;
then A326: 1 <= i0 -' 1 by A30, A45, A321, NAT_1:13;
A327: j1 -' 1 = j0 by A321, NAT_D:34;
A328: (i1 -' 1) + (1 + 1) = i2 by A45, A322;
A329: 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, A321, A326, 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, A321, A324, A326, A327, A328, 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 A330: 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, A325, A329, Th4, NAT_1:13;
 i1 -' 1 <= i1 by NAT_D:35;
then A331: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2;
A332: Int (cell ((GoB f),(i1 -' 1),j1)) is convex by A27, A331, Th17;
 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 A30, A55, A321, A330, A19, A45, A324, A326, GOBOARD6:83, Th4, A332;
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 ((((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, A321, A324, A326, 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, A321, A324, A326, A328, 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 A336: 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, A333, A335, Th4;
A337: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A334, A336, A20, A23, A322, A324, GOBOARD6:83, Th4, A337; ::_thesis: verum
end;
supposethat 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;
 width (GoB f) > j1 by A27, A341, XXREAL_0:1;
then A343: width (GoB f) >= j1 + 1 by NAT_1:13;
A344: i0 -' 1 = 0 by A340, XREAL_1:232;
A345: 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, A338, A340, A344, 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, A338, A340, A343, 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 A346: 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, A342, A345, Th4, NAT_1:13;
 i1 -' 1 <= i1 by NAT_D:35;
then A347: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2;
A348: Int (cell ((GoB f),(i1 -' 1),j1)) is convex by A27, A347, Th17;
 Int (cell ((GoB f),(i1 -' 1),j1)) misses L~ f by A27, A347, GOBOARD7:12;
then  Int (cell ((GoB f),(i1 -' 1),j1)) c= (L~ f) ` by SUBSET_1:23;
then A349: Int (cell ((GoB f),(i1 -' 1),j1)) c= LeftComp f by A30, A55, A338, A346, A26, A340, A343, A344, GOBOARD6:85, Th4, A348;
A350: left_cell (f,(k + 1)) = cell ((GoB f),i1,j1) by A4, A5, A13, A14, A16, A17, A31, A338, A339, GOBOARD5:28;
A351: 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, A338, A340, A343, A344, 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, A338, A339, A340, A343, 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 A352: 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, A349, A351, Th4;
A353: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A350, A352, A20, A23, A26, A338, A339, A343, GOBOARD6:82, Th4, A353; ::_thesis: verum
end;
supposethat A354: j0 + 1 = j1 and
A355: i1 + 1 = i2 and
A356: i0 <> 1 and
A357: j1 <> width (GoB f) ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A358: left_cell (f,k) = cell ((GoB f),(i1 -' 1),j0) by A6, A7, A10, A11, A13, A14, A30, A45, A354, GOBOARD5:27;
 1 < i0 by A18, A356, XXREAL_0:1;
then A359: 1 <= i0 -' 1 by A30, A45, A354, NAT_1:13;
 width (GoB f) > j1 by A27, A357, XXREAL_0:1;
then A360: width (GoB f) >= j1 + 1 by NAT_1:13;
A361: (i1 -' 1) + (1 + 1) = i2 by A45, A355;
A362: 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, A354, A359, 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, A354, A359, A360, A361, 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 A363: 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, A358, A362, Th4, NAT_1:13;
 i1 -' 1 <= i1 by NAT_D:35;
then A364: i1 -' 1 <= len (GoB f) by A21, XXREAL_0:2;
A365: Int (cell ((GoB f),(i1 -' 1),j1)) is convex by A27, A364, Th17;
 Int (cell ((GoB f),(i1 -' 1),j1)) misses L~ f by A27, A364, GOBOARD7:12;
then  Int (cell ((GoB f),(i1 -' 1),j1)) c= (L~ f) ` by SUBSET_1:23;
then A366: Int (cell ((GoB f),(i1 -' 1),j1)) c= LeftComp f by A30, A55, A354, A363, A19, A26, A45, A359, A360, GOBOARD6:82, Th4, A365;
A367: left_cell (f,(k + 1)) = cell ((GoB f),i1,j1) by A4, A5, A13, A14, A16, A17, A31, A354, A355, GOBOARD5:28;
A368: 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, A354, A359, A360, 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, A354, A359, A360, A361, 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 A369: 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, A366, A368, Th4;
A370: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A367, A369, A20, A23, A26, A355, A360, GOBOARD6:82, Th4, A370; ::_thesis: verum
end;
supposethat A371: j0 + 1 = j1 and
A372: j1 + 1 = j2 and
A373: i0 = 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A374: left_cell (f,k) = cell ((GoB f),0,j0) by A6, A7, A10, A11, A13, A14, A30, A56, A371, A373, GOBOARD5:27;
A375: left_cell (f,(k + 1)) = cell ((GoB f),0,j1) by A4, A5, A13, A14, A16, A17, A30, A31, A56, A371, A372, A373, GOBOARD5:27;
A376: 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, A371, 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, A371, A372, 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 A377: 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, A374, A376, Th4, NAT_1:13;
A378: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A55, A375, A377, A26, A29, A372, GOBOARD6:85, Th4, A378; ::_thesis: verum
end;
supposethat A379: j0 + 1 = j1 and
A380: j1 + 1 = j2 and
A381: i0 <> 1 ; ::_thesis: Int (left_cell (f,(k + 1))) c= LeftComp f
A382: left_cell (f,k) = cell ((GoB f),(i1 -' 1),j0) by A6, A7, A10, A11, A13, A14, A30, A45, A379, GOBOARD5:27;
 1 < i0 by A18, A381, XXREAL_0:1;
then A383: 1 <= i0 -' 1 by A30, A45, A379, NAT_1:13;
A384: left_cell (f,(k + 1)) = cell ((GoB f),(i1 -' 1),j1) by A4, A5, A13, A14, A16, A17, A31, A45, A380, GOBOARD5:27;
A385: 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, A379, A383, 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, A379, A380, A383, 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 A386: 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, A382, A385, Th4, NAT_1:13;
A387: Int (left_cell (f,(k + 1))) is convex by A4, A5, Th19;
 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 A30, A55, A379, A384, A386, A19, A26, A29, A45, A380, A383, GOBOARD6:82, Th4, A387; ::_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 S1[k] from NAT_1:sch_1(A1, A2); ::_thesis: verum
end;

theorem :: GOBOARD9:22
for f being non constant standard special_circular_sequence holds GoB (Rev f) = GoB f by Lm1;

theorem Th23: :: GOBOARD9:23
for f being non constant standard special_circular_sequence holds RightComp f = LeftComp (Rev f)
proof
let f be non constant standard special_circular_sequence; ::_thesis: RightComp f = LeftComp (Rev f)
 LeftComp (Rev f) is_a_component_of (L~ (Rev f)) ` by Def1;
then A1: LeftComp (Rev f) is_a_component_of (L~ f) ` by SPPOL_2:22;
A2: len f >= 4 by GOBOARD7:34;
A3: len f >= 1 + 1 by GOBOARD7:34, XXREAL_0:2;
A4: ((len f) -' 1) + 1 = len f by A2, XREAL_1:235, XXREAL_0:2;
then A5: 1 <= (len f) -' 1 by A3, XREAL_1:6;
A6: ((len f) -' 1) + 1 <= len (Rev f) by A4, FINSEQ_5:def_3;
 right_cell (f,1) = left_cell ((Rev f),((len f) -' 1)) by A4, A5, Th10;
then  Int (right_cell (f,1)) c= LeftComp (Rev f) by A5, A6, Th21;
hence  RightComp f = LeftComp (Rev f) by A1, Def2; ::_thesis: verum
end;

theorem :: GOBOARD9:24
for f being non constant standard special_circular_sequence holds RightComp (Rev f) = LeftComp f
proof
let f be non constant standard special_circular_sequence; ::_thesis: RightComp (Rev f) = LeftComp f
 Rev (Rev f) = f ;
hence  RightComp (Rev f) = LeftComp f by Th23; ::_thesis: verum
end;

theorem :: GOBOARD9:25
for f being non constant standard special_circular_sequence
for k being Element of NAT st 1 <= k & k + 1 <= len f holds
Int (right_cell (f,k)) c= RightComp f
proof
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 (right_cell (f,k)) c= RightComp f
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len f implies Int (right_cell (f,k)) c= RightComp f )
assume that
A1: 1 <= k and
A2: k + 1 <= len f ; ::_thesis: Int (right_cell (f,k)) c= RightComp f
A3: len f = len (Rev f) by FINSEQ_5:def_3;
 k <= len f by A2, NAT_1:13;
then A4: ((len f) -' k) + k = len f by XREAL_1:235;
then A5: 1 <= (len f) -' k by A2, XREAL_1:6;
A6: ((len f) -' k) + 1 <= len f by A1, A4, XREAL_1:6;
A7: right_cell (f,k) = left_cell ((Rev f),((len f) -' k)) by A1, A4, A5, Th10;
 RightComp f = LeftComp (Rev f) by Th23;
hence  Int (right_cell (f,k)) c= RightComp f by A3, A5, A6, A7, Th21; ::_thesis: verum
end;