:: SPRECT_4 semantic presentation

begin


theorem Th1: :: SPRECT_4:1
for f being S-Sequence_in_R2
for Q being closed Subset of (TOP-REAL 2) st L~ f meets Q & not f /. 1 in Q holds
(L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}
proof
let f be S-Sequence_in_R2; ::_thesis: for Q being closed Subset of (TOP-REAL 2) st L~ f meets Q & not f /. 1 in Q holds
(L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}
let Q be closed Subset of (TOP-REAL 2); ::_thesis: ( L~ f meets Q & not f /. 1 in Q implies (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} )
assume that
A1: L~ f meets Q and
A2: not f /. 1 in Q ; ::_thesis: (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}
set p1 = f /. 1;
set p2 = f /. (len f);
set fp = First_Point ((L~ f),(f /. 1),(f /. (len f)),Q);
A3: (L~ f) /\ Q is closed by TOPS_1:8;
 len f >= 1 + 1 by TOPREAL1:def_8;
then A4: len f > 1 by NAT_1:13;
 L~ f is_an_arc_of f /. 1,f /. (len f) by TOPREAL1:25;
then A5: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A3, JORDAN5C:def_1;
then A6: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in L~ f by XBOOLE_0:def_4;
then A7: 1 <= Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) by JORDAN3:8;
A8: Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) <= len f by A6, JORDAN3:8;
then A9: Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) in dom f by A7, FINSEQ_3:25;
A10: now__::_thesis:_(L~_(R_Cut_(f,(First_Point_((L~_f),(f_/._1),(f_/._(len_f)),Q)))))_/\_Q_c=_{(First_Point_((L~_f),(f_/._1),(f_/._(len_f)),Q))}
assume  not (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q c= {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} ; ::_thesis: contradiction
then consider q being set  such that
A11: q in (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q and
A12: not q in {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} by TARSKI:def_3;
reconsider q = q as Point of (TOP-REAL 2) by A11;
A13: q in L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A11, XBOOLE_0:def_4;
A14: L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) c= L~ f by A6, JORDAN3:41;
A15: q <> First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) by A12, TARSKI:def_1;
 q in Q by A11, XBOOLE_0:def_4;
then A16: LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) by A3, A13, A14, JORDAN5C:15;
percases ( First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = f . 1 or First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . 1 ) ;
supposeA17: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = f . 1 ; ::_thesis: contradiction
A18: len <*(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))*> = 1 by FINSEQ_1:39;
 q in L~ <*(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))*> by A13, A17, JORDAN3:def_4;
hence  contradiction by A18, TOPREAL1:22; ::_thesis: verum
end;
supposeA19: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . 1 ; ::_thesis: contradiction
set m = mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)));
A20: Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) < len f by A6, JORDAN3:8;
 len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) = ((Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) -' 1) + 1 by A7, A8, JORDAN4:8;
then A21: not mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))) is empty by CARD_1:27, NAT_1:11;
A22: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))) by A6, JORDAN3:9;
 q in L~ ((mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) ^ <*(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))*>) by A13, A19, JORDAN3:def_4;
then A23: q in (L~ (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))))) \/ (LSeg (((mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) /. (len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))))),(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A21, SPPOL_2:19;
now__::_thesis:_contradiction
percases ( q in L~ (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) or q in LSeg (((mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) /. (len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))))),(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))) ) by A23, XBOOLE_0:def_3;
supposeA24: q in L~ (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) ; ::_thesis: contradiction
A25: now__::_thesis:_not_Index_((First_Point_((L~_f),(f_/._1),(f_/._(len_f)),Q)),f)_<=_1
assume  Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) <= 1 ; ::_thesis: contradiction
then  Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) = 1 by A7, XXREAL_0:1;
then  len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) = 1 by A4, JORDAN4:15;
hence  contradiction by A24, TOPREAL1:22; ::_thesis: verum
end;
then A26: LE q,f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)), L~ f,f /. 1,f /. (len f) by A8, A24, SPRECT_3:17;
 f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) in LSeg ((f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))),(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))) by RLTOPSP1:68;
then  LE f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)), First_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) by A20, A22, A25, SPRECT_3:23;
then  LE q, First_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) by A26, JORDAN5C:13;
hence  contradiction by A15, A16, JORDAN5C:12, TOPREAL1:25; ::_thesis: verum
end;
supposeA27: q in LSeg (((mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) /. (len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))))),(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))) ; ::_thesis: contradiction
 len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) in dom (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) by A21, FINSEQ_5:6;
then (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) /. (len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))))) = (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)))) . (len (mid (f,1,(Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))))) by PARTFUN1:def_6
.= f . (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) by A7, A8, JORDAN4:10
.= f /. (Index ((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) by A9, PARTFUN1:def_6 ;
then  LE q, First_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) by A7, A20, A22, A27, SPRECT_3:23;
hence  contradiction by A15, A16, JORDAN5C:12, TOPREAL1:25; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
end;
end;
A28: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in Q by A5, XBOOLE_0:def_4;
 1 in dom f by A4, FINSEQ_3:25;
then  First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . 1 by A2, A28, PARTFUN1:def_6;
then  First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A6, JORDAN5B:20;
then  First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q by A28, XBOOLE_0:def_4;
hence  (L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} by A10, ZFMISC_1:33; ::_thesis: verum
end;

theorem :: SPRECT_4:2
for f being non empty FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is being_S-Seq & p = f /. (len f) holds
L~ (L_Cut (f,p)) = {}
proof
let f be non empty FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st f is being_S-Seq & p = f /. (len f) holds
L~ (L_Cut (f,p)) = {}
let p be Point of (TOP-REAL 2); ::_thesis: ( f is being_S-Seq & p = f /. (len f) implies L~ (L_Cut (f,p)) = {} )
assume that
A1: f is being_S-Seq and
A2: p = f /. (len f) ; ::_thesis: L~ (L_Cut (f,p)) = {}
 len f >= 2 by A1, TOPREAL1:def_8;
then  len f >= 1 by XXREAL_0:2;
then  len f in dom f by FINSEQ_3:25;
then  p = f . (len f) by A2, PARTFUN1:def_6;
then  L_Cut (f,p) = <*p*> by A1, JORDAN5B:17;
then  len (L_Cut (f,p)) = 1 by FINSEQ_1:39;
hence  L~ (L_Cut (f,p)) = {} by TOPREAL1:22; ::_thesis: verum
end;

theorem Th3: :: SPRECT_4:3
for f being S-Sequence_in_R2
for p being Point of (TOP-REAL 2)
for j being Element of NAT st 1 <= j & j < len f & p in L~ (mid (f,j,(len f))) holds
LE f /. j,p, L~ f,f /. 1,f /. (len f)
proof
let f be S-Sequence_in_R2; ::_thesis: for p being Point of (TOP-REAL 2)
for j being Element of NAT st 1 <= j & j < len f & p in L~ (mid (f,j,(len f))) holds
LE f /. j,p, L~ f,f /. 1,f /. (len f)
let p be Point of (TOP-REAL 2); ::_thesis: for j being Element of NAT st 1 <= j & j < len f & p in L~ (mid (f,j,(len f))) holds
LE f /. j,p, L~ f,f /. 1,f /. (len f)
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < len f & p in L~ (mid (f,j,(len f))) implies LE f /. j,p, L~ f,f /. 1,f /. (len f) )
assume that
A1: 1 <= j and
A2: j < len f and
A3: p in L~ (mid (f,j,(len f))) ; ::_thesis: LE f /. j,p, L~ f,f /. 1,f /. (len f)
consider i being Element of NAT  such that
A4: 1 <= i and
A5: i + 1 <= len (mid (f,j,(len f))) and
A6: p in LSeg ((mid (f,j,(len f))),i) by A3, SPPOL_2:13;
A7: len (mid (f,j,(len f))) = ((len f) -' j) + 1 by A1, A2, JORDAN4:8;
then  i <= (len f) -' j by A5, XREAL_1:6;
then A8: i + j <= len f by A2, NAT_D:54;
 j + i >= i by NAT_1:11;
then A9: ((j + i) -' 1) + 1 <= len f by A4, A8, XREAL_1:235, XXREAL_0:2;
 1 + 1 <= j + i by A1, A4, XREAL_1:7;
then A10: 1 <= (j + i) -' 1 by NAT_D:49;
 j + 1 <= j + i by A4, XREAL_1:6;
then A11: j <= (j + i) -' 1 by NAT_D:49;
 ((j + i) -' 1) + 1 >= (j + i) -' 1 by NAT_1:11;
then  len f >= (j + i) -' 1 by A9, XXREAL_0:2;
then A12: LE f /. j,f /. ((j + i) -' 1), L~ f,f /. 1,f /. (len f) by A1, A11, JORDAN5C:24;
 i < ((len f) -' j) + 1 by A5, A7, NAT_1:13;
then  p in LSeg (f,((j + i) -' 1)) by A1, A2, A4, A6, JORDAN4:19;
then  LE f /. ((j + i) -' 1),p, L~ f,f /. 1,f /. (len f) by A10, A9, JORDAN5C:25;
hence  LE f /. j,p, L~ f,f /. 1,f /. (len f) by A12, JORDAN5C:13; ::_thesis: verum
end;

theorem Th4: :: SPRECT_4:4
for f being S-Sequence_in_R2
for p, q being Point of (TOP-REAL 2)
for j being Element of NAT st 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg (p,(f /. (j + 1))) holds
LE p,q, L~ f,f /. 1,f /. (len f)
proof
let f be S-Sequence_in_R2; ::_thesis: for p, q being Point of (TOP-REAL 2)
for j being Element of NAT st 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg (p,(f /. (j + 1))) holds
LE p,q, L~ f,f /. 1,f /. (len f)
let p, q be Point of (TOP-REAL 2); ::_thesis: for j being Element of NAT st 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg (p,(f /. (j + 1))) holds
LE p,q, L~ f,f /. 1,f /. (len f)
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg (p,(f /. (j + 1))) implies LE p,q, L~ f,f /. 1,f /. (len f) )
assume that
A1: 1 <= j and
A2: j < len f and
A3: p in LSeg (f,j) and
A4: q in LSeg (p,(f /. (j + 1))) ; ::_thesis: LE p,q, L~ f,f /. 1,f /. (len f)
A5: j + 1 <= len f by A2, NAT_1:13;
then A6: LSeg (f,j) = LSeg ((f /. j),(f /. (j + 1))) by A1, TOPREAL1:def_3;
A7: f /. (j + 1) in LSeg (f,j) by A1, A5, TOPREAL1:21;
then A8: LSeg (p,(f /. (j + 1))) c= LSeg (f,j) by A3, A6, TOPREAL1:6;
then A9: q in LSeg (f,j) by A4;
A10: LSeg (f,j) c= L~ f by TOPREAL3:19;
percases ( p = q or q <> p ) ;
suppose p = q ; ::_thesis: LE p,q, L~ f,f /. 1,f /. (len f)
hence  LE p,q, L~ f,f /. 1,f /. (len f) by A3, A10, JORDAN5C:9; ::_thesis: verum
end;
supposeA11: q <> p ; ::_thesis: LE p,q, L~ f,f /. 1,f /. (len f)
 for i, j being Element of NAT st p in LSeg (f,i) & q in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds
( i <= j & ( i = j implies LE p,q,f /. i,f /. (i + 1) ) )
proof
 1 <= j + 1 by NAT_1:11;
then A12: j + 1 in dom f by A5, FINSEQ_3:25;
let i1, i2 be Element of NAT ; ::_thesis: ( p in LSeg (f,i1) & q in LSeg (f,i2) & 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f implies ( i1 <= i2 & ( i1 = i2 implies LE p,q,f /. i1,f /. (i1 + 1) ) ) )
assume that
A13: p in LSeg (f,i1) and
A14: q in LSeg (f,i2) and
 1 <= i1 and
A15: i1 + 1 <= len f and
A16: 1 <= i2 and
 i2 + 1 <= len f ; ::_thesis: ( i1 <= i2 & ( i1 = i2 implies LE p,q,f /. i1,f /. (i1 + 1) ) )
A17: p in (LSeg (f,i1)) /\ (LSeg (f,j)) by A3, A13, XBOOLE_0:def_4;
then A18: LSeg (f,i1) meets LSeg (f,j) by XBOOLE_0:4;
then A19: i1 + 1 >= j by TOPREAL1:def_7;
A20: now__::_thesis:_not_j_+_1_=_i1
A21: j + (1 + 1) = (j + 1) + 1 ;
assume  j + 1 = i1 ; ::_thesis: contradiction
then  p in {(f /. (j + 1))} by A1, A15, A17, A21, TOPREAL1:def_6;
then  p = f /. (j + 1) by TARSKI:def_1;
then  q in {p} by A4, RLTOPSP1:70;
hence  contradiction by A11, TARSKI:def_1; ::_thesis: verum
end;
A22: now__::_thesis:_(_i2_+_1_>_j_&_j_+_1_>_i2_implies_i2_=_j_)
assume that
A23: i2 + 1 > j and
A24: j + 1 > i2 ; ::_thesis: i2 = j
A25: j <= i2 by A23, NAT_1:13;
 i2 <= j by A24, NAT_1:13;
hence  i2 = j by A25, XXREAL_0:1; ::_thesis: verum
end;
A26: now__::_thesis:_(_i1_+_1_>_j_&_j_+_1_>_i1_implies_i1_=_j_)
assume that
A27: i1 + 1 > j and
A28: j + 1 > i1 ; ::_thesis: i1 = j
A29: j <= i1 by A27, NAT_1:13;
 i1 <= j by A28, NAT_1:13;
hence  i1 = j by A29, XXREAL_0:1; ::_thesis: verum
end;
A30: q in (LSeg (f,i2)) /\ (LSeg (f,j)) by A4, A8, A14, XBOOLE_0:def_4;
then A31: LSeg (f,i2) meets LSeg (f,j) by XBOOLE_0:4;
then A32: j + 1 >= i2 by TOPREAL1:def_7;
A33: j in dom f by A1, A2, FINSEQ_3:25;
A34: now__::_thesis:_not_f_/._(j_+_1)_=_f_/._j
assume  f /. (j + 1) = f /. j ; ::_thesis: contradiction
then  j = j + 1 by A12, A33, PARTFUN2:10;
hence  contradiction ; ::_thesis: verum
end;
A35: now__::_thesis:_not_i2_+_1_=_j
A36: i2 + (1 + 1) = (i2 + 1) + 1 ;
assume  i2 + 1 = j ; ::_thesis: contradiction
then  q in {(f /. j)} by A5, A16, A30, A36, TOPREAL1:def_6;
then  q = f /. j by TARSKI:def_1;
hence  contradiction by A3, A4, A6, A7, A11, A34, SPPOL_1:7, TOPREAL1:6; ::_thesis: verum
end;
 i2 + 1 >= j by A31, TOPREAL1:def_7;
then  ( i2 + 1 = j or i2 = j or j + 1 = i2 ) by A22, A32, XXREAL_0:1;
then A37: i2 >= j by A35, NAT_1:11;
A38: j + 1 >= i1 by A18, TOPREAL1:def_7;
then  ( i1 + 1 = j or i1 = j ) by A26, A19, A20, XXREAL_0:1;
then  i1 <= j by NAT_1:11;
hence  i1 <= i2 by A37, XXREAL_0:2; ::_thesis: ( i1 = i2 implies LE p,q,f /. i1,f /. (i1 + 1) )
assume A39: i1 = i2 ; ::_thesis: LE p,q,f /. i1,f /. (i1 + 1)
 not p in LSeg (q,(f /. (j + 1))) by A4, A11, SPRECT_3:6;
then  not LE q,p,f /. j,f /. (j + 1) by JORDAN3:30;
then  LT p,q,f /. j,f /. (j + 1) by A3, A6, A14, A26, A19, A38, A20, A34, A35, A39, JORDAN3:28, XXREAL_0:1;
hence  LE p,q,f /. i1,f /. (i1 + 1) by A26, A19, A38, A20, A35, A39, JORDAN3:def_6, XXREAL_0:1; ::_thesis: verum
end;
hence  LE p,q, L~ f,f /. 1,f /. (len f) by A3, A9, A10, A11, JORDAN5C:30; ::_thesis: verum
end;
end;
end;

theorem Th5: :: SPRECT_4:5
for f being S-Sequence_in_R2
for Q being closed Subset of (TOP-REAL 2) st L~ f meets Q & not f /. (len f) in Q holds
(L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}
proof
let f be S-Sequence_in_R2; ::_thesis: for Q being closed Subset of (TOP-REAL 2) st L~ f meets Q & not f /. (len f) in Q holds
(L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}
let Q be closed Subset of (TOP-REAL 2); ::_thesis: ( L~ f meets Q & not f /. (len f) in Q implies (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} )
assume that
A1: L~ f meets Q and
A2: not f /. (len f) in Q ; ::_thesis: (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}
set p1 = f /. 1;
set p2 = f /. (len f);
set lp = Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q);
A3: (L~ f) /\ Q is closed by TOPS_1:8;
 len f >= 1 + 1 by TOPREAL1:def_8;
then A4: len f > 1 by NAT_1:13;
 L~ f is_an_arc_of f /. 1,f /. (len f) by TOPREAL1:25;
then A5: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A3, JORDAN5C:def_2;
then A6: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in L~ f by XBOOLE_0:def_4;
then A7: 1 <= Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) by JORDAN3:8;
A8: now__::_thesis:_(L~_(L_Cut_(f,(Last_Point_((L~_f),(f_/._1),(f_/._(len_f)),Q)))))_/\_Q_c=_{(Last_Point_((L~_f),(f_/._1),(f_/._(len_f)),Q))}
set m = mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f));
assume  not (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q c= {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} ; ::_thesis: contradiction
then consider q being set  such that
A9: q in (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q and
A10: not q in {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} by TARSKI:def_3;
reconsider q = q as Point of (TOP-REAL 2) by A9;
A11: q in L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A9, XBOOLE_0:def_4;
A12: L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) c= L~ f by A6, JORDAN3:42;
A13: Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f) < len f by A6, JORDAN3:8;
then A14: (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 <= len f by NAT_1:13;
A15: 1 <= (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 by NAT_1:11;
then  len (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) = ((len f) -' ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1)) + 1 by A14, JORDAN4:8;
then A16: not mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f)) is empty by CARD_1:27, NAT_1:11;
A17: q <> Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) by A10, TARSKI:def_1;
 q in Q by A9, XBOOLE_0:def_4;
then A18: LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) by A3, A11, A12, JORDAN5C:16;
percases ( Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) or Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) ) ;
suppose Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) ; ::_thesis: contradiction
then A19: q in L~ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) by A11, JORDAN3:def_3;
now__::_thesis:_not_(Index_((Last_Point_((L~_f),(f_/._1),(f_/._(len_f)),Q)),f))_+_1_>=_len_f
assume  (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 >= len f ; ::_thesis: contradiction
then  (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 = len f by A14, XXREAL_0:1;
then  len (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) = 1 by A4, JORDAN4:15;
hence  contradiction by A19, TOPREAL1:22; ::_thesis: verum
end;
then A20: LE f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),q, L~ f,f /. 1,f /. (len f) by A19, Th3, NAT_1:11;
A21: f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) in LSeg ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),(f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1))) by RLTOPSP1:68;
 Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))) by A6, JORDAN3:9;
then  LE Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1), L~ f,f /. 1,f /. (len f) by A7, A13, A21, Th4;
then  LE Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) by A20, JORDAN5C:13;
hence  contradiction by A17, A18, JORDAN5C:12, TOPREAL1:25; ::_thesis: verum
end;
supposeA22: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) ; ::_thesis: contradiction
A23: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,(Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f))) by A6, JORDAN3:9;
 1 <= (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 by NAT_1:11;
then A24: (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 in dom f by A14, FINSEQ_3:25;
 q in L~ (<*(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))*> ^ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f)))) by A11, A22, JORDAN3:def_3;
then A25: q in (L~ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f)))) \/ (LSeg (((mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) /. 1),(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A16, SPPOL_2:20;
now__::_thesis:_contradiction
percases ( q in L~ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) or q in LSeg ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),((mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) /. 1)) ) by A25, XBOOLE_0:def_3;
supposeA26: q in L~ (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) ; ::_thesis: contradiction
now__::_thesis:_not_(Index_((Last_Point_((L~_f),(f_/._1),(f_/._(len_f)),Q)),f))_+_1_>=_len_f
assume  (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 >= len f ; ::_thesis: contradiction
then  (Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1 = len f by A14, XXREAL_0:1;
then  len (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) = 1 by A4, JORDAN4:15;
hence  contradiction by A26, TOPREAL1:22; ::_thesis: verum
end;
then A27: LE f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),q, L~ f,f /. 1,f /. (len f) by A26, Th3, NAT_1:11;
 f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) in LSeg ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),(f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1))) by RLTOPSP1:68;
then  LE Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1), L~ f,f /. 1,f /. (len f) by A7, A13, A23, Th4;
then  LE Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) by A27, JORDAN5C:13;
hence  contradiction by A17, A18, JORDAN5C:12, TOPREAL1:25; ::_thesis: verum
end;
supposeA28: q in LSeg ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),((mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) /. 1)) ; ::_thesis: contradiction
 1 in dom (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) by A16, FINSEQ_5:6;
then (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) /. 1 = (mid (f,((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1),(len f))) . 1 by PARTFUN1:def_6
.= f . ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) by A4, A14, A15, FINSEQ_6:118
.= f /. ((Index ((Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)),f)) + 1) by A24, PARTFUN1:def_6 ;
then  LE Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) by A7, A13, A23, A28, Th4;
hence  contradiction by A17, A18, JORDAN5C:12, TOPREAL1:25; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
end;
end;
A29: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in Q by A5, XBOOLE_0:def_4;
 len f in dom f by A4, FINSEQ_3:25;
then  Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> f . (len f) by A2, A29, PARTFUN1:def_6;
then  Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q)))) by A6, JORDAN5B:19;
then  Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q by A29, XBOOLE_0:def_4;
hence  (L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))} by A8, ZFMISC_1:33; ::_thesis: verum
end;

 Lm1:  for f being non constant standard clockwise_oriented special_circular_sequence st f /. 1 = N-min (L~ f) holds
LeftComp f <> RightComp f
proof
let f be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( f /. 1 = N-min (L~ f) implies LeftComp f <> RightComp f )
set A = N-min (L~ f);
assume that
A1: f /. 1 = N-min (L~ f) and
A2: LeftComp f = RightComp f ; ::_thesis: contradiction
A3: LeftComp (SpStSeq (L~ f)) c= LeftComp f by A1, SPRECT_3:41;
consider i being Element of NAT  such that
A4: 1 <= i and
A5: i < len (GoB f) and
A6: N-min (L~ f) = (GoB f) * (i,(width (GoB f))) by SPRECT_3:28;
set w = width (GoB f);
A7: len f > 4 by GOBOARD7:34;
A8: 1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
A9: width (GoB f) > 1 by GOBOARD7:33;
then A10: ((width (GoB f)) -' 1) + 1 = width (GoB f) by XREAL_1:235;
A11: [i,(width (GoB f))] in Indices (GoB f) by A4, A5, A9, MATRIX_1:36;
A12: 1 <= i + 1 by NAT_1:11;
A13: i + 1 <= len (GoB f) by A5, NAT_1:13;
then A14: [(i + 1),(width (GoB f))] in Indices (GoB f) by A9, A12, MATRIX_1:36;
A15: 1 in dom f by FINSEQ_5:6;
A16: i in dom (GoB f) by A4, A5, FINSEQ_3:25;
then A17: f /. (1 + 1) = (GoB f) * ((i + 1),(width (GoB f))) by A1, A6, SPRECT_3:29;
then A18: right_cell (f,1) = cell ((GoB f),i,((width (GoB f)) -' 1)) by A1, A6, A8, A10, A11, A14, GOBOARD5:28;
set z2 = (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))));
set p1 = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))));
set p2 = (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))));
A19: 1 <= (width (GoB f)) -' 1 by GOBOARD7:33, NAT_D:49;
then A20: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) in Int (cell ((GoB f),i,((width (GoB f)) -' 1))) by A4, A10, A13, GOBOARD6:31;
A21: Int (right_cell (f,1)) c= RightComp f by A8, GOBOARD9:25;
A22: W-bound (L~ (SpStSeq (L~ f))) = W-bound (L~ f) by SPRECT_1:58;
A23: S-bound (L~ (SpStSeq (L~ f))) = S-bound (L~ f) by SPRECT_1:59;
A24: N-bound (L~ (SpStSeq (L~ f))) = N-bound (L~ f) by SPRECT_1:60;
A25: E-bound (L~ (SpStSeq (L~ f))) = E-bound (L~ f) by SPRECT_1:61;
A26: 1 < i + 1 by A4, NAT_1:13;
A27: 1 <= len (GoB f) by A4, A5, XXREAL_0:2;
A28: (width (GoB f)) -' 1 < width (GoB f) by A10, XREAL_1:29;
A29: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) = (1 / 2) * ((N-min (L~ f)) + ((GoB f) * ((i + 1),((width (GoB f)) -' 1)))) by A4, A6, A10, A13, A19, GOBOARD7:9;
then A30: ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `1 = (1 / 2) * (((N-min (L~ f)) + ((GoB f) * ((i + 1),((width (GoB f)) -' 1)))) `1) by TOPREAL3:4
.= (1 / 2) * (((N-min (L~ f)) `1) + (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1)) by TOPREAL3:2
.= ((1 / 2) * ((N-min (L~ f)) `1)) + ((1 / 2) * (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1)) ;
A31: ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2 = (1 / 2) * (((N-min (L~ f)) + ((GoB f) * ((i + 1),((width (GoB f)) -' 1)))) `2) by A29, TOPREAL3:4
.= (1 / 2) * (((N-min (L~ f)) `2) + (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2)) by TOPREAL3:2
.= (1 / 2) * ((N-bound (L~ f)) + (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2)) by EUCLID:52
.= ((1 / 2) * (N-bound (L~ f))) + ((1 / 2) * (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2)) ;
A32: ((1 / 2) * (W-bound (L~ f))) + ((1 / 2) * (W-bound (L~ f))) = W-bound (L~ f) ;
A33: ((1 / 2) * (S-bound (L~ f))) + ((1 / 2) * (S-bound (L~ f))) = S-bound (L~ f) ;
A34: ((1 / 2) * (N-bound (L~ f))) + ((1 / 2) * (N-bound (L~ f))) = N-bound (L~ f) ;
A35: ((1 / 2) * (E-bound (L~ f))) + ((1 / 2) * (E-bound (L~ f))) = E-bound (L~ f) ;
 N-min (L~ f) in L~ f by SPRECT_1:11;
then  (N-min (L~ f)) `1 >= W-bound (L~ f) by PSCOMP_1:24;
then A36: (1 / 2) * ((N-min (L~ f)) `1) >= (1 / 2) * (W-bound (L~ f)) by XREAL_1:64;
A37: ((GoB f) * (1,((width (GoB f)) -' 1))) `1 = ((GoB f) * (1,1)) `1 by A19, A27, A28, GOBOARD5:2;
 ((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1 > ((GoB f) * (1,((width (GoB f)) -' 1))) `1 by A13, A19, A26, A28, GOBOARD5:3;
then  ((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1 > W-bound (L~ f) by A37, JORDAN5D:37;
then  (1 / 2) * (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1) > (1 / 2) * (W-bound (L~ f)) by XREAL_1:68;
then A38: W-bound (L~ (SpStSeq (L~ f))) < ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `1 by A22, A30, A32, A36, XREAL_1:8;
 N-max (L~ f) in L~ f by SPRECT_1:11;
then  (N-max (L~ f)) `1 <= E-bound (L~ f) by PSCOMP_1:24;
then  (N-min (L~ f)) `1 < E-bound (L~ f) by SPRECT_2:51, XXREAL_0:2;
then A39: (1 / 2) * ((N-min (L~ f)) `1) < (1 / 2) * (E-bound (L~ f)) by XREAL_1:68;
A40: ((GoB f) * ((len (GoB f)),((width (GoB f)) -' 1))) `1 = ((GoB f) * ((len (GoB f)),1)) `1 by A19, A27, A28, GOBOARD5:2;
 ((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1 <= ((GoB f) * ((len (GoB f)),((width (GoB f)) -' 1))) `1 by A12, A13, A19, A28, SPRECT_3:13;
then  ((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1 <= E-bound (L~ f) by A40, JORDAN5D:39;
then  (1 / 2) * (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `1) <= (1 / 2) * (E-bound (L~ f)) by XREAL_1:64;
then A41: ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `1 < E-bound (L~ (SpStSeq (L~ f))) by A25, A30, A35, A39, XREAL_1:8;
A42: (1 / 2) * (N-bound (L~ f)) > (1 / 2) * (S-bound (L~ f)) by SPRECT_1:32, XREAL_1:68;
A43: ((GoB f) * ((i + 1),1)) `2 = ((GoB f) * (1,1)) `2 by A9, A12, A13, GOBOARD5:1;
 ((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2 >= ((GoB f) * ((i + 1),1)) `2 by A12, A13, A19, A28, SPRECT_3:12;
then  ((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2 >= S-bound (L~ f) by A43, JORDAN5D:38;
then  (1 / 2) * (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2) >= (1 / 2) * (S-bound (L~ f)) by XREAL_1:64;
then A44: S-bound (L~ (SpStSeq (L~ f))) < ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2 by A23, A31, A33, A42, XREAL_1:8;
A45: ((GoB f) * ((i + 1),(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A9, A12, A13, GOBOARD5:1;
 ((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2 < ((GoB f) * ((i + 1),(width (GoB f)))) `2 by A12, A13, A19, A28, GOBOARD5:4;
then  ((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2 < N-bound (L~ f) by A45, JORDAN5D:40;
then  (1 / 2) * (((GoB f) * ((i + 1),((width (GoB f)) -' 1))) `2) < (1 / 2) * (N-bound (L~ f)) by XREAL_1:68;
then A46: ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2 < N-bound (L~ (SpStSeq (L~ f))) by A24, A31, A34, XREAL_1:6;
 RightComp (SpStSeq (L~ f)) =  {  q where q is Point of (TOP-REAL 2) : ( W-bound (L~ (SpStSeq (L~ f))) < q `1 & q `1 < E-bound (L~ (SpStSeq (L~ f))) & S-bound (L~ (SpStSeq (L~ f))) < q `2 & q `2 < N-bound (L~ (SpStSeq (L~ f))) )  }  by SPRECT_3:37;
then A47: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) in RightComp (SpStSeq (L~ f)) by A38, A41, A44, A46;
consider z1 being set  such that
A48: z1 in LeftComp (SpStSeq (L~ f)) by XBOOLE_0:def_1;
 LeftComp (SpStSeq (L~ f)) misses RightComp (SpStSeq (L~ f)) by SPRECT_1:88;
then A49: z1 <> (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A47, A48, XBOOLE_0:3;
reconsider z1 = z1 as Point of (TOP-REAL 2) by A48;
consider P being Subset of (TOP-REAL 2) such that
A50: P is_S-P_arc_joining z1,(1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) and
A51: P c= RightComp f by A2, A3, A18, A20, A21, A48, A49, TOPREAL4:29;
consider Red9 being FinSequence of (TOP-REAL 2) such that
A52: Red9 is being_S-Seq and
A53: P = L~ Red9 and
A54: z1 = Red9 /. 1 and
A55: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) = Red9 /. (len Red9) by A50, TOPREAL4:def_1;
A56: L~ (SpStSeq (L~ f)) meets L~ Red9 by A47, A48, A52, A54, A55, SPRECT_3:33;
A57: 2 in dom f by A8, FINSEQ_3:25;
A58: len f in dom f by FINSEQ_5:6;
A59: (len f) -' 1 >= 1 by A8, NAT_D:49;
 (len f) -' 1 <= len f by NAT_D:44;
then A60: (len f) -' 1 in dom f by A59, FINSEQ_3:25;
 1 <= len f by A58, FINSEQ_3:25;
then A61: ((len f) -' 1) + 1 = len f by XREAL_1:235;
then A62: (len f) -' 1 < len f by NAT_1:13;
A63: <*(NW-corner (L~ f))*> is_in_the_area_of f by SPRECT_2:26;
A64: (width (GoB f)) -' 1 < width (GoB f) by A10, NAT_1:13;
then  Int (cell ((GoB f),i,((width (GoB f)) -' 1))) misses L~ (SpStSeq (L~ f)) by A4, A5, A19, SPRECT_3:55;
then A65: not (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) in L~ (SpStSeq (L~ f)) by A20, XBOOLE_0:3;
A66: LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) c= L~ (SpStSeq (L~ f)) by SPRECT_3:14;
A67: f /. 1 = f /. (len f) by FINSEQ_6:def_1;
A68: NW-corner (L~ f) in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by RLTOPSP1:68;
A69: N-min (L~ f) in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by SPRECT_3:15;
then A70: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A68, TOPREAL1:6;
A71: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) is horizontal by A70, SPRECT_1:9;
 1 + 2 <= len f by GOBOARD7:34, XXREAL_0:2;
then A72: (LSeg (f,1)) /\ (LSeg (f,(1 + 1))) = {(f /. (1 + 1))} by TOPREAL1:def_6;
 len f >= 2 + 1 by GOBOARD7:34, XXREAL_0:2;
then  (len f) -' 1 >= 1 + 1 by NAT_D:49;
then  ((len f) -' 1) -' 1 >= 1 by NAT_D:49;
then A73: (len f) -' 2 >= 1 by NAT_D:45;
A74: ((len f) -' 2) + 1 = (((len f) -' 1) -' 1) + 1 by NAT_D:45
.= (len f) -' 1 by A59, XREAL_1:235 ;
 ((len f) -' 2) + 2 = len f by A7, XREAL_1:235, XXREAL_0:2;
then A75: (LSeg (f,((len f) -' 1))) /\ (LSeg (f,((len f) -' 2))) = {(f /. ((len f) -' 1))} by A73, A74, TOPREAL1:def_6;
A76: f /. 2 in N-most (L~ f) by A1, SPRECT_2:30;
 N-most (L~ f) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by XBOOLE_1:17;
then A77: LSeg ((f /. 1),(f /. 2)) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A1, A69, A76, TOPREAL1:6;
A78: ((GoB f) * (i,((width (GoB f)) -' 1))) `1 = ((GoB f) * (i,1)) `1 by A4, A5, A19, A64, GOBOARD5:2
.= (N-min (L~ f)) `1 by A4, A5, A6, A9, GOBOARD5:2 ;
A79: ((GoB f) * ((i + 1),(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A9, A12, A13, GOBOARD5:1
.= (N-min (L~ f)) `2 by A4, A5, A6, A9, GOBOARD5:1 ;
then A80: (f /. 2) `2 = N-bound (L~ f) by A17, EUCLID:52;
A81: <*((GoB f) * ((i + 1),(width (GoB f))))*> is_in_the_area_of f by A9, A12, A13, SPRECT_3:49;
 <*((GoB f) * (i,((width (GoB f)) -' 1)))*> is_in_the_area_of f by A4, A5, A19, A64, SPRECT_3:49;
then  <*((GoB f) * (i,((width (GoB f)) -' 1))),((GoB f) * ((i + 1),(width (GoB f))))*> is_in_the_area_of f by A81, SPRECT_3:42;
then  <*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> is_in_the_area_of f by SPRECT_3:50;
then A82: <*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> is_in_the_area_of SpStSeq (L~ f) by SPRECT_3:53;
A83: (GoB f) * (i,((width (GoB f)) -' 1)) = f /. ((len f) -' 1) by A1, A6, A16, SPRECT_3:29;
then  LSeg ((N-min (L~ f)),(f /. ((len f) -' 1))) is vertical by A78, SPPOL_1:16;
then A84: (LSeg ((N-min (L~ f)),(f /. ((len f) -' 1)))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) = {(N-min (L~ f))} by A70, SPRECT_1:9, SPRECT_3:10;
A85: (NW-corner (L~ f)) `2 = (N-min (L~ f)) `2 by PSCOMP_1:37;
A86: (NW-corner (L~ f)) `1 <= (N-min (L~ f)) `1 by PSCOMP_1:38;
 (N-min (L~ f)) `1 <= (f /. 2) `1 by A76, PSCOMP_1:39;
then  N-min (L~ f) in LSeg ((NW-corner (L~ f)),(f /. 2)) by A17, A79, A85, A86, GOBOARD7:8;
then A87: (LSeg ((N-min (L~ f)),(f /. 2))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) = {(N-min (L~ f))} by TOPREAL1:8;
((GoB f) * (i,(width (GoB f)))) `2 = ((GoB f) * (1,(width (GoB f)))) `2 by A4, A5, A9, GOBOARD5:1
.= ((GoB f) * ((i + 1),(width (GoB f)))) `2 by A9, A12, A13, GOBOARD5:1 ;
then (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) `2 = (((GoB f) * (i,((width (GoB f)) -' 1))) `2) + (((GoB f) * ((i + 1),(width (GoB f)))) `2) by TOPREAL3:2
.= (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) `2 by TOPREAL3:2 ;
then ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))) `2 = (1 / 2) * ((((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) `2) by TOPREAL3:4
.= ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2 by TOPREAL3:4 ;
then A88: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) is horizontal by SPPOL_1:15;
A89: f /. ((len f) -' 1) in LSeg ((f /. ((len f) -' 1)),(f /. (len f))) by RLTOPSP1:68;
A90: (GoB f) * (i,(width (GoB f))) = f /. (len f) by A1, A6, FINSEQ_6:def_1;
 (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) = ((1 / 2) * ((GoB f) * (i,((width (GoB f)) -' 1)))) + ((1 - (1 / 2)) * ((GoB f) * (i,(width (GoB f))))) by EUCLID:32;
then A91: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) in LSeg ((f /. ((len f) -' 1)),(f /. (len f))) by A83, A90;
then A92: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) c= LSeg ((f /. ((len f) -' 1)),(f /. (len f))) by A89, TOPREAL1:6;
 LSeg ((f /. ((len f) -' 1)),(f /. (len f))) = LSeg (f,((len f) -' 1)) by A59, A61, TOPREAL1:def_3;
then A93: LSeg ((f /. ((len f) -' 1)),(f /. (len f))) c= L~ f by TOPREAL3:19;
then A94: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) c= L~ f by A92, XBOOLE_1:1;
A95: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) c= LSeg (f,((len f) -' 1)) by A59, A61, A92, TOPREAL1:def_3;
A96: ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))) `1 = (1 / 2) * ((((GoB f) * (i,((width (GoB f)) -' 1))) + (N-min (L~ f))) `1) by A6, TOPREAL3:4
.= (1 / 2) * (((N-min (L~ f)) `1) + ((N-min (L~ f)) `1)) by A78, TOPREAL3:2
.= (N-min (L~ f)) `1 ;
then A97: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) is vertical by A78, A83, SPPOL_1:16;
A98: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by RLTOPSP1:68;
then A99: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) in L~ f by A94;
A100: now__::_thesis:_not_(1_/_2)_*_(((GoB_f)_*_(i,((width_(GoB_f))_-'_1)))_+_((GoB_f)_*_(i,(width_(GoB_f)))))_=_N-min_(L~_f)
assume  (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) = N-min (L~ f) ; ::_thesis: contradiction
then  f /. ((len f) -' 1) = f /. (len f) by A1, A6, A67, A83, SPRECT_3:5;
hence  contradiction by A58, A60, A61, GOBOARD7:29; ::_thesis: verum
end;
 (1 + 1) + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
then A101: 1 + 1 <= (len f) -' 1 by NAT_D:49;
then A102: 1 <= ((len f) -' 1) -' 1 by NAT_D:49;
A103: (((len f) -' 1) -' 1) + 1 = (len f) -' 1 by A101, XREAL_1:235, XXREAL_0:2;
A104: (((len f) -' 1) -' 1) + 2 = ((len f) -' 2) + 2 by NAT_D:45
.= len f by A7, XREAL_1:235, XXREAL_0:2 ;
A105: for i, j being Element of NAT st 1 <= i & i <= j & j < (len f) -' 1 holds
L~ (mid (f,i,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))
proof
let l, j be Element of NAT ; ::_thesis: ( 1 <= l & l <= j & j < (len f) -' 1 implies L~ (mid (f,l,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) )
assume that
A106: 1 <= l and
A107: l <= j and
A108: j < (len f) -' 1 ; ::_thesis: L~ (mid (f,l,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))
assume  L~ (mid (f,l,j)) meets LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) ; ::_thesis: contradiction
then  (L~ (mid (f,l,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) <> {} by XBOOLE_0:def_7;
then consider p being Point of (TOP-REAL 2) such that
A109: p in (L~ (mid (f,l,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) by SUBSET_1:4;
 p in L~ (mid (f,l,j)) by A109, XBOOLE_0:def_4;
then consider ii being Element of NAT  such that
A110: 1 <= ii and
A111: ii + 1 <= len (mid (f,l,j)) and
A112: p in LSeg ((mid (f,l,j)),ii) by SPPOL_2:13;
 (len f) -' 1 > l by A107, A108, XXREAL_0:2;
then  (len f) -' 1 > 1 by A106, XXREAL_0:2;
then A113: (len f) -' 1 < len f by NAT_D:51;
then A114: j < len f by A108, XXREAL_0:2;
then  len (mid (f,l,j)) = (j -' l) + 1 by A106, A107, JORDAN4:8;
then A115: ii < (j -' l) + 1 by A111, NAT_1:13;
set k = (ii + l) -' 1;
A116: p in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A109, XBOOLE_0:def_4;
percases ( l = j or l < j ) by A107, XXREAL_0:1;
suppose l = j ; ::_thesis: contradiction
then  len (mid (f,l,j)) = 1 by A106, A114, JORDAN4:15;
then  L~ (mid (f,l,j)) = {} by TOPREAL1:22;
hence  contradiction by A112, SPPOL_2:17; ::_thesis: verum
end;
supposeA117: l < j ; ::_thesis: contradiction
A118: ii + 1 >= 1 + 1 by A110, XREAL_1:6;
 ii + l >= ii + 1 by A106, XREAL_1:6;
then A119: ii + l >= 1 + 1 by A118, XXREAL_0:2;
then A120: (ii + l) -' 1 >= 1 by NAT_D:49;
A121: ii + l >= 1 by A119, XXREAL_0:2;
A122: now__::_thesis:_not_((ii_+_l)_-'_1)_+_1_>=_(len_f)_-'_1
assume  ((ii + l) -' 1) + 1 >= (len f) -' 1 ; ::_thesis: contradiction
then  (ii + l) -' 1 >= ((len f) -' 1) -' 1 by NAT_D:53;
then A123: ii + l >= (len f) -' 1 by A121, NAT_D:56;
 ii + l < ((j -' l) + 1) + l by A115, XREAL_1:6;
then  ii + l < ((j -' l) + l) + 1 ;
then  ii + l < j + 1 by A117, XREAL_1:235;
then  (len f) -' 1 < j + 1 by A123, XXREAL_0:2;
hence  contradiction by A108, NAT_1:13; ::_thesis: verum
end;
A124: (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)} by JORDAN4:42
.= {(f /. 1)} by A15, PARTFUN1:def_6 ;
 LSeg ((mid (f,l,j)),ii) = LSeg (f,((ii + l) -' 1)) by A106, A114, A110, A115, A117, JORDAN4:19;
then A125: p in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (f,((len f) -' 1))) by A95, A116, A112, XBOOLE_0:def_4;
then  LSeg (f,((ii + l) -' 1)) meets LSeg (f,((len f) -' 1)) by XBOOLE_0:4;
then  (ii + l) -' 1 <= 1 by A113, A122, GOBOARD5:def_4;
then  (ii + l) -' 1 = 1 by A120, XXREAL_0:1;
then  p = f /. 1 by A125, A124, TARSKI:def_1;
hence  contradiction by A1, A67, A91, A100, A116, SPRECT_3:6; ::_thesis: verum
end;
end;
end;
A126: for j being Element of NAT st 1 <= j & j < (len f) -' 1 holds
(L~ (mid (f,j,((len f) -' 1)))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) = {(f /. ((len f) -' 1))}
proof
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < (len f) -' 1 implies (L~ (mid (f,j,((len f) -' 1)))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) = {(f /. ((len f) -' 1))} )
assume that
A127: 1 <= j and
A128: j < (len f) -' 1 ; ::_thesis: (L~ (mid (f,j,((len f) -' 1)))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) = {(f /. ((len f) -' 1))}
A129: 1 <= (len f) -' 1 by A127, A128, XXREAL_0:2;
A130: ((len f) -' 1) -' 1 = (len f) -' 2 by NAT_D:45;
then A131: L~ (mid (f,j,((len f) -' 1))) = (LSeg (f,((len f) -' 2))) \/ (L~ (mid (f,j,((len f) -' 2)))) by A127, A128, NAT_D:35, SPRECT_3:20;
 j <= (len f) -' 2 by A128, A130, NAT_D:49;
then  LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) misses L~ (mid (f,j,((len f) -' 2))) by A105, A127, A129, A130, JORDAN5B:1;
hence (L~ (mid (f,j,((len f) -' 1)))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) = (LSeg (f,((len f) -' 2))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) by A131, XBOOLE_1:78
.= {(f /. ((len f) -' 1))} by A75, A95, RLTOPSP1:68, ZFMISC_1:124 ;
::_thesis: verum
end;
A132: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses LSeg ((f /. ((len f) -' 1)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))
proof
assume  LSeg ((NW-corner (L~ f)),(N-min (L~ f))) meets LSeg ((f /. ((len f) -' 1)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) ; ::_thesis: contradiction
then  (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) <> {} by XBOOLE_0:def_7;
then consider p being Point of (TOP-REAL 2) such that
A133: p in (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) by SUBSET_1:4;
A134: p in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A133, XBOOLE_0:def_4;
 p in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A133, XBOOLE_0:def_4;
then  p in {(N-min (L~ f))} by A1, A67, A84, A92, A134, XBOOLE_0:def_4;
then  p = N-min (L~ f) by TARSKI:def_1;
hence  contradiction by A1, A67, A91, A100, A134, SPRECT_3:6; ::_thesis: verum
end;
A135: ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))) `2 <> (N-min (L~ f)) `2 by A96, A100, TOPREAL3:6;
set G = GoB f;
A136: Int (cell ((GoB f),i,((width (GoB f)) -' 1))) misses L~ f by A5, A64, GOBOARD7:12;
(L~ f) /\ ((Int (cell ((GoB f),i,((width (GoB f)) -' 1)))) \/ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))}) = ((L~ f) /\ (Int (cell ((GoB f),i,((width (GoB f)) -' 1))))) \/ ((L~ f) /\ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))}) by XBOOLE_1:23
.= {} \/ ((L~ f) /\ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))}) by A136, XBOOLE_0:def_7
.= (L~ f) /\ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} ;
then A137: (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) /\ (L~ f) c= (L~ f) /\ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} by A4, A5, A10, A19, A64, GOBOARD6:40, XBOOLE_1:26;
 (L~ f) /\ {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} c= {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} by XBOOLE_1:17;
then A138: (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) /\ (L~ f) c= {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} by A137, XBOOLE_1:1;
A139: for i, j being Element of NAT st 1 <= i & i < j & j < len f holds
L~ (mid (f,i,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))
proof
 len f >= 1 + 1 by GOBOARD7:34, XXREAL_0:2;
then A140: (len f) -' 1 >= 1 by NAT_D:49;
let l, j be Element of NAT ; ::_thesis: ( 1 <= l & l < j & j < len f implies L~ (mid (f,l,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) )
assume that
A141: 1 <= l and
A142: l < j and
A143: j < len f ; ::_thesis: L~ (mid (f,l,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))
assume  L~ (mid (f,l,j)) meets LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) ; ::_thesis: contradiction
then  (L~ (mid (f,l,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) <> {} by XBOOLE_0:def_7;
then consider p being Point of (TOP-REAL 2) such that
A144: p in (L~ (mid (f,l,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) by SUBSET_1:4;
 p in L~ (mid (f,l,j)) by A144, XBOOLE_0:def_4;
then consider ii being Element of NAT  such that
A145: 1 <= ii and
A146: ii + 1 <= len (mid (f,l,j)) and
A147: p in LSeg ((mid (f,l,j)),ii) by SPPOL_2:13;
A148: len (mid (f,l,j)) = (j -' l) + 1 by A141, A142, A143, JORDAN4:8;
then  ii < (j -' l) + 1 by A146, NAT_1:13;
then A149: p in LSeg (f,((ii + l) -' 1)) by A141, A142, A143, A145, A147, JORDAN4:19;
set k = (ii + l) -' 1;
A150: ii + 1 >= 1 + 1 by A145, XREAL_1:6;
 (LSeg (f,((ii + l) -' 1))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) c= (L~ f) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) by TOPREAL3:19, XBOOLE_1:26;
then A151: (LSeg (f,((ii + l) -' 1))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) c= {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} by A138, XBOOLE_1:1;
 p in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A144, XBOOLE_0:def_4;
then  p in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) by A149, XBOOLE_0:def_4;
then  p = (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) by A151, TARSKI:def_1;
then  (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) in (LSeg (f,((ii + l) -' 1))) /\ (LSeg ((f /. ((len f) -' 1)),(f /. (len f)))) by A91, A149, XBOOLE_0:def_4;
then A152: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (f,((len f) -' 1))) by A61, A140, TOPREAL1:def_3;
then A153: LSeg (f,((ii + l) -' 1)) meets LSeg (f,((len f) -' 1)) by XBOOLE_0:4;
 ii + l >= ii + 1 by A141, XREAL_1:6;
then  ii + l >= 1 + 1 by A150, XXREAL_0:2;
then A154: (ii + l) -' 1 >= 1 by NAT_D:49;
percases ( (ii + l) -' 1 <= 1 or ((ii + l) -' 1) + 1 >= (len f) -' 1 ) by A62, A153, GOBOARD5:def_4;
supposeA155: (ii + l) -' 1 <= 1 ; ::_thesis: contradiction
A156: (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)} by JORDAN4:42
.= {(f /. 1)} by A15, PARTFUN1:def_6 ;
 (ii + l) -' 1 = 1 by A154, A155, XXREAL_0:1;
hence  contradiction by A1, A100, A152, A156, TARSKI:def_1; ::_thesis: verum
end;
supposeA157: ((ii + l) -' 1) + 1 >= (len f) -' 1 ; ::_thesis: contradiction
 ii <= j -' l by A146, A148, XREAL_1:6;
then  ii + l <= j by A142, NAT_D:54;
then A158: ii + l < len f by A143, XXREAL_0:2;
 ii + l >= l by NAT_1:11;
then  ii + l >= 1 by A141, XXREAL_0:2;
then  (ii + l) -' 1 < (len f) -' 1 by A158, NAT_D:56;
then A159: (ii + l) -' 1 <= ((len f) -' 1) -' 1 by NAT_D:49;
 (ii + l) -' 1 >= ((len f) -' 1) -' 1 by A157, NAT_D:53;
then  (ii + l) -' 1 = ((len f) -' 1) -' 1 by A159, XXREAL_0:1;
then  (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) in {(f /. ((len f) -' 1))} by A102, A103, A104, A152, TOPREAL1:def_6;
then  (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) = f /. ((len f) -' 1) by TARSKI:def_1;
hence  contradiction by A6, A83, A100, SPRECT_3:5; ::_thesis: verum
end;
end;
end;
A160: <*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))*> is_in_the_area_of f by A94, A98, SPRECT_2:21, SPRECT_3:46;
then A161: <*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))*> is_in_the_area_of SpStSeq (L~ f) by SPRECT_3:53;
 <*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> = <*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))*> ^ <*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> by FINSEQ_1:def_9;
then A162: (L~ (SpStSeq (L~ f))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) c= {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} by A65, A82, A161, SPRECT_2:24, SPRECT_3:47;
((GoB f) * (i,((width (GoB f)) -' 1))) `1 = ((GoB f) * (i,1)) `1 by A4, A5, A19, GOBOARD5:2, NAT_D:35
.= ((GoB f) * (i,(width (GoB f)))) `1 by A4, A5, A9, GOBOARD5:2 ;
then (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) `1 = (((GoB f) * (i,((width (GoB f)) -' 1))) `1) + (((GoB f) * ((i + 1),(width (GoB f)))) `1) by TOPREAL3:2
.= (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) `1 by TOPREAL3:2 ;
then ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `1 = (1 / 2) * ((((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) `1) by TOPREAL3:4
.= ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `1 by TOPREAL3:4 ;
then A163: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) is vertical by SPPOL_1:16;
A164: f /. 2 in LSeg ((f /. 1),(f /. (1 + 1))) by RLTOPSP1:68;
 (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) = ((1 / 2) * ((GoB f) * (i,(width (GoB f))))) + ((1 - (1 / 2)) * ((GoB f) * ((i + 1),(width (GoB f))))) by EUCLID:32;
then A165: (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in LSeg ((f /. 1),(f /. 2)) by A1, A6, A17;
then A166: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) c= LSeg ((f /. 1),(f /. 2)) by A164, TOPREAL1:6;
A167: LSeg ((f /. 1),(f /. (1 + 1))) = LSeg (f,1) by A8, TOPREAL1:def_3;
then A168: LSeg ((f /. 1),(f /. 2)) c= L~ f by TOPREAL3:19;
then A169: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) c= L~ f by A166, XBOOLE_1:1;
A170: ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `2 = (1 / 2) * (((N-min (L~ f)) + ((GoB f) * ((i + 1),(width (GoB f))))) `2) by A6, TOPREAL3:4
.= (1 / 2) * (((N-min (L~ f)) `2) + ((N-min (L~ f)) `2)) by A79, TOPREAL3:2
.= N-bound (L~ f) by EUCLID:52 ;
A171: (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by RLTOPSP1:68;
A172: (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) <> N-min (L~ f) by A1, A6, A15, A17, A57, GOBOARD7:29, SPRECT_3:5;
A173: for i, j being Element of NAT st 2 < i & i <= j & j <= len f holds
L~ (mid (f,i,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))
proof
let l, j be Element of NAT ; ::_thesis: ( 2 < l & l <= j & j <= len f implies L~ (mid (f,l,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) )
assume that
A174: 2 < l and
A175: l <= j and
A176: j <= len f ; ::_thesis: L~ (mid (f,l,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))
assume  L~ (mid (f,l,j)) meets LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) ; ::_thesis: contradiction
then  (L~ (mid (f,l,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) <> {} by XBOOLE_0:def_7;
then consider p being Point of (TOP-REAL 2) such that
A177: p in (L~ (mid (f,l,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) by SUBSET_1:4;
A178: p in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by A177, XBOOLE_0:def_4;
 p in L~ (mid (f,l,j)) by A177, XBOOLE_0:def_4;
then consider ii being Element of NAT  such that
A179: 1 <= ii and
A180: ii + 1 <= len (mid (f,l,j)) and
A181: p in LSeg ((mid (f,l,j)),ii) by SPPOL_2:13;
A182: 1 < l by A174, XXREAL_0:2;
then A183: len (mid (f,l,j)) = (j -' l) + 1 by A175, A176, JORDAN4:8;
then A184: ii < (j -' l) + 1 by A180, NAT_1:13;
set k = (ii + l) -' 1;
A185: ii + 2 >= 1 + 2 by A179, XREAL_1:6;
 ii + l > ii + 2 by A174, XREAL_1:6;
then  ii + l > 1 + 2 by A185, XXREAL_0:2;
then A186: (ii + l) -' 1 > 1 + 1 by NAT_D:52;
percases ( l = j or l < j ) by A175, XXREAL_0:1;
suppose l = j ; ::_thesis: contradiction
then  len (mid (f,l,j)) = 1 by A176, A182, JORDAN4:15;
then  L~ (mid (f,l,j)) = {} by TOPREAL1:22;
hence  contradiction by A181, SPPOL_2:17; ::_thesis: verum
end;
supposeA187: l < j ; ::_thesis: contradiction
A188: (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)} by JORDAN4:42
.= {(f /. 1)} by A15, PARTFUN1:def_6 ;
 ii <= j -' l by A180, A183, XREAL_1:6;
then  ii + l <= j by A175, NAT_D:54;
then  ii + l <= len f by A176, XXREAL_0:2;
then A189: (ii + l) -' 1 <= (len f) -' 1 by NAT_D:42;
 LSeg ((mid (f,l,j)),ii) = LSeg (f,((ii + l) -' 1)) by A176, A182, A179, A184, A187, JORDAN4:19;
then A190: p in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (f,1)) by A166, A167, A178, A181, XBOOLE_0:def_4;
then  LSeg (f,((ii + l) -' 1)) meets LSeg (f,1) by XBOOLE_0:4;
then  ((ii + l) -' 1) + 1 >= len f by A186, GOBOARD5:def_4;
then  (ii + l) -' 1 >= (len f) -' 1 by NAT_D:53;
then  (ii + l) -' 1 = (len f) -' 1 by A189, XXREAL_0:1;
then  p = f /. 1 by A190, A188, TARSKI:def_1;
hence  contradiction by A1, A165, A172, A178, SPRECT_3:6; ::_thesis: verum
end;
end;
end;
A191: for j being Element of NAT st 2 < j & j <= len f holds
(L~ (mid (f,2,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) = {(f /. 2)}
proof
A192: f /. 2 in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by RLTOPSP1:68;
let j be Element of NAT ; ::_thesis: ( 2 < j & j <= len f implies (L~ (mid (f,2,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) = {(f /. 2)} )
assume that
A193: 2 < j and
A194: j <= len f ; ::_thesis: (L~ (mid (f,2,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) = {(f /. 2)}
 2 + 1 <= j by A193, NAT_1:13;
then A195: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) misses L~ (mid (f,(2 + 1),j)) by A173, A194;
 L~ (mid (f,2,j)) = (LSeg (f,2)) \/ (L~ (mid (f,(2 + 1),j))) by A193, A194, SPRECT_3:19;
hence (L~ (mid (f,2,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) = (LSeg (f,2)) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) by A195, XBOOLE_1:78
.= {(f /. 2)} by A72, A164, A165, A167, A192, TOPREAL1:6, ZFMISC_1:124 ;
::_thesis: verum
end;
A196: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) misses LSeg ((NW-corner (L~ f)),(N-min (L~ f)))
proof
assume  LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) meets LSeg ((NW-corner (L~ f)),(N-min (L~ f))) ; ::_thesis: contradiction
then  (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) <> {} by XBOOLE_0:def_7;
then consider p being Point of (TOP-REAL 2) such that
A197: p in (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) by SUBSET_1:4;
A198: p in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by A197, XBOOLE_0:def_4;
 p in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A197, XBOOLE_0:def_4;
then  p in {(N-min (L~ f))} by A1, A87, A166, A198, XBOOLE_0:def_4;
then  p = N-min (L~ f) by TARSKI:def_1;
hence  contradiction by A1, A165, A172, A198, SPRECT_3:6; ::_thesis: verum
end;
A199: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))
proof
assume  LSeg ((NW-corner (L~ f)),(N-min (L~ f))) meets LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) ; ::_thesis: contradiction
then  (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) <> {} by XBOOLE_0:def_7;
then consider p being Point of (TOP-REAL 2) such that
A200: p in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) by SUBSET_1:4;
A201: p in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A200, XBOOLE_0:def_4;
A202: p in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A200, XBOOLE_0:def_4;
 (LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) = {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A77, A163, A165, SPRECT_3:11;
then  p in {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A70, A202, A201, XBOOLE_0:def_4;
then  (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A202, TARSKI:def_1;
then  (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ f) by A169, A171, XBOOLE_0:def_4;
then  (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in {(N-min (L~ f))} by PSCOMP_1:43;
hence  contradiction by A172, TARSKI:def_1; ::_thesis: verum
end;
A203: for i, j being Element of NAT st 1 < i & i < j & j <= len f holds
L~ (mid (f,i,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))
proof
A204: len f >= 2 by GOBOARD7:34, XXREAL_0:2;
A205: Int (cell ((GoB f),i,((width (GoB f)) -' 1))) misses L~ f by A5, A64, GOBOARD7:12;
A206: (L~ f) /\ {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} c= {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by XBOOLE_1:17;
let l, j be Element of NAT ; ::_thesis: ( 1 < l & l < j & j <= len f implies L~ (mid (f,l,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) )
assume that
A207: 1 < l and
A208: l < j and
A209: j <= len f ; ::_thesis: L~ (mid (f,l,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))
assume  L~ (mid (f,l,j)) meets LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) ; ::_thesis: contradiction
then  (L~ (mid (f,l,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) <> {} by XBOOLE_0:def_7;
then consider p being Point of (TOP-REAL 2) such that
A210: p in (L~ (mid (f,l,j))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) by SUBSET_1:4;
 p in L~ (mid (f,l,j)) by A210, XBOOLE_0:def_4;
then consider ii being Element of NAT  such that
A211: 1 <= ii and
A212: ii + 1 <= len (mid (f,l,j)) and
A213: p in LSeg ((mid (f,l,j)),ii) by SPPOL_2:13;
A214: len (mid (f,l,j)) = (j -' l) + 1 by A207, A208, A209, JORDAN4:8;
then  ii < (j -' l) + 1 by A212, NAT_1:13;
then A215: p in LSeg (f,((ii + l) -' 1)) by A207, A208, A209, A211, A213, JORDAN4:19;
set k = (ii + l) -' 1;
set G = GoB f;
A216: (LSeg (f,((ii + l) -' 1))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) c= (L~ f) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) by TOPREAL3:19, XBOOLE_1:26;
(L~ f) /\ ((Int (cell ((GoB f),i,((width (GoB f)) -' 1)))) \/ {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))}) = ((L~ f) /\ (Int (cell ((GoB f),i,((width (GoB f)) -' 1))))) \/ ((L~ f) /\ {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))}) by XBOOLE_1:23
.= {} \/ ((L~ f) /\ {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))}) by A205, XBOOLE_0:def_7
.= (L~ f) /\ {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} ;
then  (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ f) c= (L~ f) /\ {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A4, A5, A10, A19, A64, GOBOARD6:41, XBOOLE_1:26;
then  (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ f) c= {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A206, XBOOLE_1:1;
then A217: (LSeg (f,((ii + l) -' 1))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) c= {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A216, XBOOLE_1:1;
 p in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A210, XBOOLE_0:def_4;
then  p in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) by A215, XBOOLE_0:def_4;
then  p = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A217, TARSKI:def_1;
then  (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in (LSeg (f,((ii + l) -' 1))) /\ (LSeg ((f /. 1),(f /. (1 + 1)))) by A165, A215, XBOOLE_0:def_4;
then A218: (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in (LSeg (f,((ii + l) -' 1))) /\ (LSeg (f,1)) by A204, TOPREAL1:def_3;
then  LSeg (f,((ii + l) -' 1)) meets LSeg (f,1) by XBOOLE_0:4;
then A219: ( (ii + l) -' 1 <= 1 + 1 or ((ii + l) -' 1) + 1 >= len f ) by GOBOARD5:def_4;
A220: ii + 1 >= 1 + 1 by A211, XREAL_1:6;
 ii + l > ii + 1 by A207, XREAL_1:6;
then  ii + l > 1 + 1 by A220, XXREAL_0:2;
then A221: (ii + l) -' 1 > 1 by NAT_D:52;
percases ( (ii + l) -' 1 <= 2 or ((ii + l) -' 1) + 1 >= len f ) by A219;
supposeA222: (ii + l) -' 1 <= 2 ; ::_thesis: contradiction
 (ii + l) -' 1 >= 1 + 1 by A221, NAT_1:13;
then A223: (ii + l) -' 1 = 2 by A222, XXREAL_0:1;
 1 + 2 <= len f by GOBOARD7:34, XXREAL_0:2;
then  (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in {(f /. (1 + 1))} by A218, A223, TOPREAL1:def_6;
then  (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) = f /. (1 + 1) by TARSKI:def_1;
hence  contradiction by A6, A17, A172, SPRECT_3:5; ::_thesis: verum
end;
supposeA224: ((ii + l) -' 1) + 1 >= len f ; ::_thesis: contradiction
A225: (LSeg (f,1)) /\ (LSeg (f,((len f) -' 1))) = {(f . 1)} by JORDAN4:42
.= {(f /. 1)} by A15, PARTFUN1:def_6 ;
 ii <= j -' l by A212, A214, XREAL_1:6;
then  ii + l <= j by A208, NAT_D:54;
then  ii + l <= len f by A209, XXREAL_0:2;
then A226: (ii + l) -' 1 <= (len f) -' 1 by NAT_D:42;
 (ii + l) -' 1 >= (len f) -' 1 by A224, NAT_D:53;
then  (ii + l) -' 1 = (len f) -' 1 by A226, XXREAL_0:1;
hence  contradiction by A1, A172, A218, A225, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
 LSeg ((f /. 1),(f /. 2)) c= L~ (SpStSeq (L~ f)) by A1, SPRECT_3:31;
then A227: (L~ (SpStSeq (L~ f))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) = {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A65, A82, A165, SPRECT_3:48;
A228: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) is horizontal by A80, A170, SPPOL_1:15;
A229: (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by RLTOPSP1:68;
then A230: (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in L~ f by A169;
A231: <*((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> is_in_the_area_of f by A169, A229, SPRECT_2:21, SPRECT_3:46;
A232: L~ f misses L~ Red9 by A51, A53, SPRECT_3:25, XBOOLE_1:63;
reconsider Red9 = Red9 as S-Sequence_in_R2 by A52;
 len Red9 in dom Red9 by FINSEQ_5:6;
then A233: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) in L~ Red9 by A55, SPPOL_2:44;
set u1 = Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))));
set Red = L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))));
set u2 = First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))));
set u3 = First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))));
 NW-corner (L~ (SpStSeq (L~ f))) = NW-corner (L~ f) by SPRECT_1:62;
then A234: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) <> NW-corner (L~ f) by A47, A48, A54, A55, SPRECT_3:38;
A235: L~ Red9 is_an_arc_of z1,(1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A54, A55, TOPREAL1:25;
 (L~ Red9) /\ (L~ (SpStSeq (L~ f))) is closed by TOPS_1:8;
then A236: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ Red9) /\ (L~ (SpStSeq (L~ f))) by A54, A55, A56, A235, JORDAN5C:def_2;
then A237: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ (SpStSeq (L~ f)) by XBOOLE_0:def_4;
A238: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ Red9 by A236, XBOOLE_0:def_4;
A239: now__::_thesis:_not_Last_Point_((L~_Red9),(Red9_/._1),(Red9_/._(len_Red9)),(L~_(SpStSeq_(L~_f))))_in_L~_f
assume  Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ f ; ::_thesis: contradiction
then  Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ f) /\ (L~ Red9) by A238, XBOOLE_0:def_4;
hence  contradiction by A232, XBOOLE_0:def_7; ::_thesis: verum
end;
 len Red9 in dom Red9 by FINSEQ_5:6;
then  Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) <> Red9 . (len Red9) by A55, A65, A237, PARTFUN1:def_6;
then reconsider Red = L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) as S-Sequence_in_R2 by A238, JORDAN3:34;
 1 in dom Red by FINSEQ_5:6;
then A240: Red /. 1 = Red . 1 by PARTFUN1:def_6
.= Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) by A238, JORDAN3:23 ;
A241: (L~ (SpStSeq (L~ f))) /\ (L~ Red) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A55, A56, A65, Th5;
 len Red9 in dom Red9 by FINSEQ_5:6;
then  (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) = Red9 . (len Red9) by A55, PARTFUN1:def_6;
then A242: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) in L~ Red by A65, A233, A237, A238, JORDAN5B:22;
 Red is_in_the_area_of SpStSeq (L~ f) by A47, A48, A54, A55, SPRECT_3:54;
then A243: Red is_in_the_area_of f by SPRECT_3:53;
A244: L~ Red c= L~ Red9 by A238, JORDAN3:42;
A245: L~ f misses L~ Red by A232, A238, JORDAN3:42, XBOOLE_1:63;
 (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by RLTOPSP1:68;
then A246: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) meets L~ Red by A242, XBOOLE_0:3;
 (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by RLTOPSP1:68;
then A247: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) meets L~ Red by A242, XBOOLE_0:3;
A248: (L~ Red) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) is closed by TOPS_1:8;
A249: (L~ Red) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) is closed by TOPS_1:8;
 L~ Red is_an_arc_of Red /. 1,Red /. (len Red) by TOPREAL1:25;
then A250: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ Red) by A247, A249, JORDAN5C:def_1;
then A251: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in L~ Red by XBOOLE_0:def_4;
A252: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A250, XBOOLE_0:def_4;
A253: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) <> (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) by A94, A98, A232, A244, A251, XBOOLE_0:3;
A254: (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by RLTOPSP1:68;
then A255: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))) c= LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A252, TOPREAL1:6;
then A256: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A71, A88, A135, SPRECT_3:9, XBOOLE_1:63;
A257: for i, j being Element of NAT st 1 <= i & i < j & j < len f holds
L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))
proof
let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i < j & j < len f implies L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) )
assume that
A258: 1 <= i and
A259: i < j and
A260: j < len f ; ::_thesis: L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))
 L~ (mid (f,i,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A139, A258, A259, A260;
hence  L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A252, A254, TOPREAL1:6, XBOOLE_1:63; ::_thesis: verum
end;
A261: now__::_thesis:_not_First_Point_((L~_(L_Cut_(Red9,(Last_Point_((L~_Red9),(Red9_/._1),(Red9_/._(len_Red9)),(L~_(SpStSeq_(L~_f)))))))),((L_Cut_(Red9,(Last_Point_((L~_Red9),(Red9_/._1),(Red9_/._(len_Red9)),(L~_(SpStSeq_(L~_f)))))))_/._1),((L_Cut_(Red9,(Last_Point_((L~_Red9),(Red9_/._1),(Red9_/._(len_Red9)),(L~_(SpStSeq_(L~_f)))))))_/._(len_(L_Cut_(Red9,(Last_Point_((L~_Red9),(Red9_/._1),(Red9_/._(len_Red9)),(L~_(SpStSeq_(L~_f))))))))),(LSeg_(((1_/_2)_*_(((GoB_f)_*_(i,((width_(GoB_f))_-'_1)))_+_((GoB_f)_*_((i_+_1),(width_(GoB_f)))))),((1_/_2)_*_(((GoB_f)_*_(i,((width_(GoB_f))_-'_1)))_+_((GoB_f)_*_(i,(width_(GoB_f)))))))))_=_Red_._1
A262: 1 in dom Red by FINSEQ_5:6;
assume  First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) = Red . 1 ; ::_thesis: contradiction
then  First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in L~ (SpStSeq (L~ f)) by A237, A240, A262, PARTFUN1:def_6;
then  First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ (SpStSeq (L~ f))) by A252, XBOOLE_0:def_4;
hence  contradiction by A162, A253, TARSKI:def_1; ::_thesis: verum
end;
 L~ Red is_an_arc_of Red /. 1,Red /. (len Red) by TOPREAL1:25;
then A263: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ Red) by A246, A248, JORDAN5C:def_1;
then A264: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in L~ Red by XBOOLE_0:def_4;
A265: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A263, XBOOLE_0:def_4;
A266: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) <> (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A169, A229, A232, A244, A264, XBOOLE_0:3;
A267: (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by RLTOPSP1:68;
then A268: LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))) c= LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A265, TOPREAL1:6;
A269: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A199, A265, A267, TOPREAL1:6, XBOOLE_1:63;
A270: for i, j being Element of NAT st 1 < i & i < j & j <= len f holds
L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))
proof
let i, j be Element of NAT ; ::_thesis: ( 1 < i & i < j & j <= len f implies L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) )
assume that
A271: 1 < i and
A272: i < j and
A273: j <= len f ; ::_thesis: L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))
 L~ (mid (f,i,j)) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A203, A271, A272, A273;
hence  L~ (mid (f,i,j)) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A265, A267, TOPREAL1:6, XBOOLE_1:63; ::_thesis: verum
end;
A274: now__::_thesis:_not_First_Point_((L~_(L_Cut_(Red9,(Last_Point_((L~_Red9),(Red9_/._1),(Red9_/._(len_Red9)),(L~_(SpStSeq_(L~_f)))))))),((L_Cut_(Red9,(Last_Point_((L~_Red9),(Red9_/._1),(Red9_/._(len_Red9)),(L~_(SpStSeq_(L~_f)))))))_/._1),((L_Cut_(Red9,(Last_Point_((L~_Red9),(Red9_/._1),(Red9_/._(len_Red9)),(L~_(SpStSeq_(L~_f)))))))_/._(len_(L_Cut_(Red9,(Last_Point_((L~_Red9),(Red9_/._1),(Red9_/._(len_Red9)),(L~_(SpStSeq_(L~_f))))))))),(LSeg_(((1_/_2)_*_(((GoB_f)_*_(i,((width_(GoB_f))_-'_1)))_+_((GoB_f)_*_((i_+_1),(width_(GoB_f)))))),((1_/_2)_*_(((GoB_f)_*_(i,(width_(GoB_f))))_+_((GoB_f)_*_((i_+_1),(width_(GoB_f)))))))))_=_Red_._1
A275: 1 in dom Red by FINSEQ_5:6;
assume  First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) = Red . 1 ; ::_thesis: contradiction
then  First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in L~ (SpStSeq (L~ f)) by A237, A240, A275, PARTFUN1:def_6;
then  First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A227, A265, XBOOLE_0:def_4;
hence  contradiction by A266, TARSKI:def_1; ::_thesis: verum
end;
reconsider Red2 = R_Cut (Red,(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))) as S-Sequence_in_R2 by A251, A261, JORDAN3:35;
A276: Red2 /. 1 = Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) by A240, A251, SPRECT_3:22;
A277: len Red2 in dom Red2 by FINSEQ_5:6;
A278: (Rev Red2) /. 1 = Red2 /. (len Red2) by FINSEQ_5:65
.= Red2 . (len Red2) by A277, PARTFUN1:def_6
.= First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) by A251, JORDAN3:24 ;
then A279: ((Rev Red2) /. 1) `2 = ((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))) `2 by A88, A252, SPPOL_1:40;
A280: (Rev Red2) /. 1 <> (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) by A94, A98, A232, A244, A251, A278, XBOOLE_0:3;
A281: L~ (Rev Red2) = L~ Red2 by SPPOL_2:22;
A282: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in L~ Red2 by A251, A261, JORDAN5B:20;
 First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))) by RLTOPSP1:68;
then A283: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) in (L~ Red2) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))))) by A282, XBOOLE_0:def_4;
now__::_thesis:_not_Last_Point_((L~_Red9),(Red9_/._1),(Red9_/._(len_Red9)),(L~_(SpStSeq_(L~_f))))_in_LSeg_(((1_/_2)_*_(((GoB_f)_*_(i,((width_(GoB_f))_-'_1)))_+_((GoB_f)_*_(i,(width_(GoB_f)))))),((1_/_2)_*_(((GoB_f)_*_(i,((width_(GoB_f))_-'_1)))_+_((GoB_f)_*_((i_+_1),(width_(GoB_f)))))))
assume  Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) ; ::_thesis: contradiction
then  Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ (SpStSeq (L~ f))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) by A237, XBOOLE_0:def_4;
hence  contradiction by A99, A162, A239, TARSKI:def_1; ::_thesis: verum
end;
then  (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ Red2) = {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))} by A240, A247, Th1;
then  (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))))) /\ (L~ Red2) c= {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))} by A252, A254, TOPREAL1:6, XBOOLE_1:26;
then  (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))))) /\ (L~ Red2) = {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))} by A283, ZFMISC_1:33;
then reconsider RB2 = <*((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))*> ^ (Rev Red2) as S-Sequence_in_R2 by A278, A279, A280, A281, SPRECT_3:16;
 LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) misses L~ Red by A92, A93, A245, XBOOLE_1:1, XBOOLE_1:63;
then  LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) misses L~ Red2 by A251, JORDAN3:41, XBOOLE_1:63;
then A284: (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) /\ (L~ Red2) = {} by XBOOLE_0:def_7;
 1 in dom Red2 by FINSEQ_5:6;
then  Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ Red2 by A276, SPPOL_2:44;
then A285: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ (SpStSeq (L~ f))) /\ (L~ Red2) by A237, XBOOLE_0:def_4;
 (L~ (SpStSeq (L~ f))) /\ (L~ Red2) c= {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A241, A251, JORDAN3:41, XBOOLE_1:26;
then A286: (L~ (SpStSeq (L~ f))) /\ (L~ Red2) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A285, ZFMISC_1:33;
reconsider Red1 = R_Cut (Red,(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))) as S-Sequence_in_R2 by A264, A274, JORDAN3:35;
 len Red1 in dom Red1 by FINSEQ_5:6;
then A287: Red1 /. (len Red1) = Red1 . (len Red1) by PARTFUN1:def_6
.= First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) by A264, JORDAN3:24 ;
A288: Red1 /. 1 = Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) by A240, A264, SPRECT_3:22;
A289: (Red1 /. (len Red1)) `1 = ((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) `1 by A163, A265, A287, SPPOL_1:41;
A290: Red1 /. (len Red1) <> (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A169, A229, A232, A244, A264, A287, XBOOLE_0:3;
A291: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in L~ Red1 by A264, A274, JORDAN5B:20;
 First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))) by RLTOPSP1:68;
then A292: First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) in (L~ Red1) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))))) by A291, XBOOLE_0:def_4;
now__::_thesis:_not_Last_Point_((L~_Red9),(Red9_/._1),(Red9_/._(len_Red9)),(L~_(SpStSeq_(L~_f))))_in_LSeg_(((1_/_2)_*_(((GoB_f)_*_(i,(width_(GoB_f))))_+_((GoB_f)_*_((i_+_1),(width_(GoB_f)))))),((1_/_2)_*_(((GoB_f)_*_(i,((width_(GoB_f))_-'_1)))_+_((GoB_f)_*_((i_+_1),(width_(GoB_f)))))))
assume  Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))))) ; ::_thesis: contradiction
then  Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ (SpStSeq (L~ f))) /\ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) by A237, XBOOLE_0:def_4;
hence  contradiction by A227, A230, A239, TARSKI:def_1; ::_thesis: verum
end;
then  (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) /\ (L~ Red1) = {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))} by A240, A246, Th1;
then  (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))))) /\ (L~ Red1) c= {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))} by A265, A267, TOPREAL1:6, XBOOLE_1:26;
then  (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))))) /\ (L~ Red1) = {(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))} by A292, ZFMISC_1:33;
then reconsider RB1 = Red1 ^ <*((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> as S-Sequence_in_R2 by A287, A289, A290, SPRECT_2:61;
 LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) misses L~ Red by A166, A168, A245, XBOOLE_1:1, XBOOLE_1:63;
then  LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) misses L~ Red1 by A264, JORDAN3:41, XBOOLE_1:63;
then A293: (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ Red1) = {} by XBOOLE_0:def_7;
 1 in dom Red1 by FINSEQ_5:6;
then A294: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ Red1 by A288, SPPOL_2:44;
then A295: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ (SpStSeq (L~ f))) /\ (L~ Red1) by A237, XBOOLE_0:def_4;
 (L~ (SpStSeq (L~ f))) /\ (L~ Red1) c= {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A241, A264, JORDAN3:41, XBOOLE_1:26;
then A296: (L~ (SpStSeq (L~ f))) /\ (L~ Red1) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A295, ZFMISC_1:33;
 len (Rev Red2) = len Red2 by FINSEQ_5:def_3;
then A297: RB2 /. (len RB2) = (Rev Red2) /. (len Red2) by SPRECT_3:1
.= Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) by A276, FINSEQ_5:65 ;
A298: RB2 /. 1 = (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))) by FINSEQ_5:15;
 L~ (Rev Red2) = L~ Red2 by SPPOL_2:22;
then A299: L~ RB2 = (L~ Red2) \/ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))))) by A278, SPPOL_2:20;
then A300: (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) /\ (L~ RB2) = {} \/ ((LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1)))) /\ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) by A284, XBOOLE_1:23
.= {((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))} by A88, A97, A255, SPRECT_1:9, SPRECT_3:10 ;
 <*(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))))*> is_in_the_area_of f by A243, A251, SPRECT_3:46;
then  Red2 is_in_the_area_of f by A243, A251, SPRECT_3:52;
then  Rev Red2 is_in_the_area_of f by SPRECT_3:51;
then A301: RB2 is_in_the_area_of f by A160, SPRECT_2:24;
 1 in dom Red1 by FINSEQ_5:6;
then A302: RB1 /. 1 = Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) by A288, FINSEQ_4:68;
 len <*((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))*> = 1 by FINSEQ_1:39;
then  len RB1 = (len Red1) + 1 by FINSEQ_1:22;
then A303: RB1 /. (len RB1) = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) by FINSEQ_4:67;
A304: L~ RB1 = (L~ Red1) \/ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) by A287, SPPOL_2:19;
then A305: (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ RB1) = {} \/ ((LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))) by A293, XBOOLE_1:23
.= {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A163, A228, A268, SPRECT_1:10, SPRECT_3:10 ;
 <*(First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))))))*> is_in_the_area_of f by A243, A264, SPRECT_3:46;
then  Red1 is_in_the_area_of f by A243, A264, SPRECT_3:52;
then A306: RB1 is_in_the_area_of f by A231, SPRECT_2:24;
A307: L~ Red9 is_an_arc_of z1,(1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A50, A53, TOPREAL4:2;
 (L~ Red9) /\ (L~ (SpStSeq (L~ f))) is closed by TOPS_1:8;
then  Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (L~ Red9) /\ (L~ (SpStSeq (L~ f))) by A54, A55, A56, A307, JORDAN5C:def_2;
then  Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in L~ (SpStSeq (L~ f)) by XBOOLE_0:def_4;
then  Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in ((LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) \/ (LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))))) \/ ((LSeg ((SE-corner (L~ f)),(SW-corner (L~ f)))) \/ (LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))))) by SPRECT_1:41;
then A308: ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (LSeg ((NW-corner (L~ f)),(NE-corner (L~ f)))) \/ (LSeg ((NE-corner (L~ f)),(SE-corner (L~ f)))) or Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (LSeg ((SE-corner (L~ f)),(SW-corner (L~ f)))) \/ (LSeg ((SW-corner (L~ f)),(NW-corner (L~ f)))) ) by XBOOLE_0:def_3;
A309: N-most (L~ f) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by XBOOLE_1:17;
A310: N-min (L~ f) in N-most (L~ f) by PSCOMP_1:42;
then  LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) = (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) \/ (LSeg ((N-min (L~ f)),(NE-corner (L~ f)))) by A309, TOPREAL1:5;
then A311: ( not Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) or Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) or Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((N-min (L~ f)),(NE-corner (L~ f))) ) by XBOOLE_0:def_3;
percases ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) or ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((N-min (L~ f)),(NE-corner (L~ f))) & N-min (L~ f) = NW-corner (L~ f) ) or ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((N-min (L~ f)),(NE-corner (L~ f))) & N-min (L~ f) <> NW-corner (L~ f) ) or ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))) & N-min (L~ f) = W-max (L~ f) ) or ( Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))) & N-min (L~ f) <> W-max (L~ f) ) or Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((SE-corner (L~ f)),(SW-corner (L~ f))) or Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))) ) by A308, A311, XBOOLE_0:def_3;
supposeA312: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) ; ::_thesis: contradiction
A313: NW-corner (L~ f) in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by RLTOPSP1:68;
then  LSeg ((NW-corner (L~ f)),(N-min (L~ f))) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A309, A310, TOPREAL1:6;
then  LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A312, A313, TOPREAL1:6;
then  LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) c= L~ (SpStSeq (L~ f)) by A66, XBOOLE_1:1;
then A314: (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (L~ Red1) c= {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A296, XBOOLE_1:26;
A315: (N-min (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
A316: NW-corner (L~ f) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by RLTOPSP1:68;
then  LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A269, A312, TOPREAL1:6, XBOOLE_1:63;
then A317: (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))) = {} by XBOOLE_0:def_7;
 Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) by RLTOPSP1:68;
then  Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (L~ Red1) by A294, XBOOLE_0:def_4;
then  {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} c= (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (L~ Red1) by ZFMISC_1:31;
then  (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (L~ Red1) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A314, XBOOLE_0:def_10;
then A318: (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /\ (L~ RB1) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} \/ {} by A304, A317, XBOOLE_1:23
.= {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} ;
 (NW-corner (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
then  (Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))) `2 = (NW-corner (L~ f)) `2 by A312, A315, GOBOARD7:6;
then reconsider M3 = <*(NW-corner (L~ f))*> ^ RB1 as S-Sequence_in_R2 by A234, A302, A318, SPRECT_3:16;
A319: L~ M3 = (LSeg ((NW-corner (L~ f)),(RB1 /. 1))) \/ (L~ RB1) by SPPOL_2:20;
set i1 = (S-min (L~ f)) .. f;
set i2 = (E-min (L~ f)) .. f;
 (N-max (L~ f)) .. f > 1 by A1, SPRECT_2:69;
then  (N-max (L~ f)) .. f >= 1 + 1 by NAT_1:13;
then  2 <= (E-max (L~ f)) .. f by A1, SPRECT_2:70, XXREAL_0:2;
then A320: 2 < (E-min (L~ f)) .. f by A1, SPRECT_2:71, XXREAL_0:2;
 LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) misses LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) by A196, A312, A316, TOPREAL1:6, XBOOLE_1:63;
then  (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) = {} by XBOOLE_0:def_7;
then A321: (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ M3) = {} \/ ((LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ RB1)) by A302, A319, XBOOLE_1:23
.= {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A305 ;
A322: L~ M3 = (LSeg ((NW-corner (L~ f)),(RB1 /. 1))) \/ (L~ RB1) by SPPOL_2:20;
 (W-min (L~ f)) .. f < len f by A1, SPRECT_2:76;
then A323: (S-min (L~ f)) .. f < len f by A1, SPRECT_2:74, XXREAL_0:2;
A324: E-min (L~ f) in rng f by SPRECT_2:45;
then A325: (E-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A326: (E-min (L~ f)) .. f <= len f by FINSEQ_3:25;
then reconsider M4 = mid (f,2,((E-min (L~ f)) .. f)) as S-Sequence_in_R2 by A320, JORDAN4:40;
 L~ M4 misses L~ Red by A57, A245, A325, SPRECT_3:18, XBOOLE_1:63;
then A327: L~ M4 misses L~ Red1 by A264, JORDAN3:41, XBOOLE_1:63;
 (S-max (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73;
then A328: (E-min (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:72, XXREAL_0:2;
then A329: 2 < (S-min (L~ f)) .. f by A320, XXREAL_0:2;
then  1 < (S-min (L~ f)) .. f by XXREAL_0:2;
then reconsider M1 = mid (f,((S-min (L~ f)) .. f),(len f)) as S-Sequence_in_R2 by A323, JORDAN4:40;
A330: L~ M1 misses L~ M4 by A328, A323, A320, SPRECT_2:47;
A331: L~ M1 misses LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by A173, A323, A329;
A332: len M1 >= 2 by TOPREAL1:def_8;
A333: M4 /. 1 = f /. 2 by A57, A325, SPRECT_2:8;
 L~ M4 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A270, A320, A326;
then A334: L~ RB1 misses L~ M4 by A304, A327, XBOOLE_1:70;
A335: LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) c= LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by A312, A316, TOPREAL1:6;
A336: now__::_thesis:_not_L~_f_meets_LSeg_((NW-corner_(L~_f)),(Last_Point_((L~_Red9),(Red9_/._1),(Red9_/._(len_Red9)),(L~_(SpStSeq_(L~_f))))))
A337: (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ f) = {(N-min (L~ f))} by PSCOMP_1:43;
assume  L~ f meets LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) ; ::_thesis: contradiction
then consider u being set  such that
A338: u in L~ f and
A339: u in LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) by XBOOLE_0:3;
reconsider u = u as Point of (TOP-REAL 2) by A338;
 u in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ f) by A335, A338, A339, XBOOLE_0:def_4;
then  u = N-min (L~ f) by A337, TARSKI:def_1;
hence  contradiction by A239, A312, A338, A339, SPRECT_3:6; ::_thesis: verum
end;
then  L~ M4 misses LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) by A57, A325, SPRECT_3:18, XBOOLE_1:63;
then A340: L~ M3 misses L~ M4 by A302, A319, A334, XBOOLE_1:70;
A341: S-min (L~ f) in rng f by SPRECT_2:41;
then A342: (S-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A343: M1 is_in_the_area_of f by A58, SPRECT_2:23;
A344: (M1 /. (len M1)) `2 = (f /. (len f)) `2 by A58, A342, SPRECT_2:9
.= (f /. 1) `2 by FINSEQ_6:def_1
.= N-bound (L~ f) by A1, EUCLID:52 ;
(M1 /. 1) `2 = (f /. ((S-min (L~ f)) .. f)) `2 by A58, A342, SPRECT_2:8
.= (S-min (L~ f)) `2 by A341, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A345: M1 is_a_v.c._for f by A343, A344, SPRECT_2:def_3;
A346: <*(NW-corner (L~ f))*> ^ RB1 is_in_the_area_of f by A63, A306, SPRECT_2:24;
 1 < (S-min (L~ f)) .. f by A329, XXREAL_0:2;
then A347: L~ M1 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A270, A323;
A348: M3 /. (len M3) = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))) by A303, SPRECT_3:1;
 (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2))) /\ (L~ M4) = {(f /. 2)} by A191, A320, A326;
then reconsider M2 = M3 ^ M4 as S-Sequence_in_R2 by A80, A170, A348, A333, A340, A321, SPRECT_3:21;
 M2 = <*(NW-corner (L~ f))*> ^ (RB1 ^ (mid (f,2,((E-min (L~ f)) .. f)))) by FINSEQ_1:32;
then A349: (M2 /. 1) `1 = (NW-corner (L~ f)) `1 by FINSEQ_5:15
.= W-bound (L~ f) by EUCLID:52 ;
 mid (f,2,((E-min (L~ f)) .. f)) is_in_the_area_of f by A57, A325, SPRECT_2:23;
then A350: M2 is_in_the_area_of f by A346, SPRECT_2:24;
(M2 /. (len M2)) `1 = ((mid (f,2,((E-min (L~ f)) .. f))) /. (len (mid (f,2,((E-min (L~ f)) .. f))))) `1 by SPRECT_3:1
.= (f /. ((E-min (L~ f)) .. f)) `1 by A57, A325, SPRECT_2:9
.= (E-min (L~ f)) `1 by A324, FINSEQ_5:38
.= E-bound (L~ f) by EUCLID:52 ;
then A351: M2 is_a_h.c._for f by A350, A349, SPRECT_2:def_2;
A352: L~ M2 = ((L~ M3) \/ (LSeg ((M3 /. (len M3)),(M4 /. 1)))) \/ (L~ M4) by SPPOL_2:23;
 len M2 >= 2 by TOPREAL1:def_8;
then  L~ M1 meets L~ M2 by A332, A345, A351, SPRECT_2:29;
then  L~ M1 meets (L~ M3) \/ (LSeg ((M3 /. (len M3)),(M4 /. 1))) by A352, A330, XBOOLE_1:70;
then A353: L~ M1 meets L~ M3 by A348, A333, A331, XBOOLE_1:70;
 L~ M1 misses LSeg ((NW-corner (L~ f)),(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))) by A58, A342, A336, SPRECT_3:18, XBOOLE_1:63;
then  L~ M1 meets L~ RB1 by A302, A353, A322, XBOOLE_1:70;
then  L~ M1 meets L~ Red1 by A304, A347, XBOOLE_1:70;
then  L~ M1 meets L~ Red by A264, JORDAN3:41, XBOOLE_1:63;
hence  contradiction by A58, A245, A342, SPRECT_3:18, XBOOLE_1:63; ::_thesis: verum
end;
supposethat A354: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((N-min (L~ f)),(NE-corner (L~ f))) and
A355: N-min (L~ f) = NW-corner (L~ f) ; ::_thesis: contradiction
set i1 = (S-max (L~ f)) .. f;
set i2 = (E-max (L~ f)) .. f;
 (N-max (L~ f)) .. f > 1 by A1, SPRECT_2:69;
then A356: 1 < (E-max (L~ f)) .. f by A1, SPRECT_2:70, XXREAL_0:2;
 (S-min (L~ f)) .. f <= (W-min (L~ f)) .. f by A1, SPRECT_2:74;
then  (S-max (L~ f)) .. f < (W-min (L~ f)) .. f by A1, SPRECT_2:73, XXREAL_0:2;
then  ((S-max (L~ f)) .. f) + 1 <= (W-min (L~ f)) .. f by NAT_1:13;
then  ((S-max (L~ f)) .. f) + 1 < len f by A1, SPRECT_2:76, XXREAL_0:2;
then A357: (S-max (L~ f)) .. f < (len f) -' 1 by A61, XREAL_1:6;
 (E-max (L~ f)) .. f < (E-min (L~ f)) .. f by A1, SPRECT_2:71;
then A358: (E-max (L~ f)) .. f < (S-max (L~ f)) .. f by A1, SPRECT_2:72, XXREAL_0:2;
then A359: 1 < (S-max (L~ f)) .. f by A356, XXREAL_0:2;
then reconsider M4 = mid (f,((S-max (L~ f)) .. f),((len f) -' 1)) as S-Sequence_in_R2 by A61, A357, JORDAN4:39;
A360: L~ M4 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A62, A257, A357, A359;
 (S-max (L~ f)) .. f < len f by A357, NAT_D:44;
then A361: (E-max (L~ f)) .. f < len f by A358, XXREAL_0:2;
then  ((E-max (L~ f)) .. f) + 1 <= len f by NAT_1:13;
then reconsider M2 = mid (f,1,((E-max (L~ f)) .. f)) as S-Sequence_in_R2 by A356, JORDAN4:39;
A362: L~ M2 misses L~ M4 by A62, A358, A357, A356, SPRECT_2:47;
 (E-max (L~ f)) .. f < (len f) -' 1 by A358, A357, XXREAL_0:2;
then A363: L~ M2 misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A105, A356;
A364: len M2 >= 2 by TOPREAL1:def_8;
A365: L~ M2 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A257, A356, A361;
A366: E-max (L~ f) in rng f by SPRECT_2:46;
then A367: (E-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then A368: (M2 /. (len M2)) `1 = (f /. ((E-max (L~ f)) .. f)) `1 by A15, SPRECT_2:9
.= (E-max (L~ f)) `1 by A366, FINSEQ_5:38
.= E-bound (L~ f) by EUCLID:52 ;
A369: S-max (L~ f) in rng f by SPRECT_2:42;
then A370: (S-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then  L~ M4 misses L~ Red by A60, A245, SPRECT_3:18, XBOOLE_1:63;
then  L~ M4 misses L~ Red2 by A251, JORDAN3:41, XBOOLE_1:63;
then A371: L~ RB2 misses L~ M4 by A299, A360, XBOOLE_1:70;
A372: M2 is_in_the_area_of f by A15, A367, SPRECT_2:23;
(M2 /. 1) `1 = (f /. 1) `1 by A15, A367, SPRECT_2:8
.= W-bound (L~ f) by A1, A355, EUCLID:52 ;
then A373: M2 is_a_h.c._for f by A372, A368, SPRECT_2:def_2;
A374: (N-min (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
A375: (NE-corner (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
A376: M4 /. (len M4) = f /. ((len f) -' 1) by A60, A370, SPRECT_2:9;
then  (LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) /\ (L~ M4) = {(M4 /. (len M4))} by A126, A357, A359;
then reconsider M1 = M4 ^ RB2 as S-Sequence_in_R2 by A78, A83, A96, A298, A300, A376, A371, SPRECT_3:21;
 mid (f,((S-max (L~ f)) .. f),((len f) -' 1)) is_in_the_area_of f by A60, A370, SPRECT_2:23;
then A377: M1 is_in_the_area_of f by A301, SPRECT_2:24;
A378: (M1 /. (len M1)) `2 = (RB2 /. (len RB2)) `2 by SPRECT_3:1
.= N-bound (L~ f) by A297, A354, A375, A374, GOBOARD7:6 ;
 not mid (f,((S-max (L~ f)) .. f),((len f) -' 1)) is empty by A60, A370, SPRECT_2:7;
then  1 in dom (mid (f,((S-max (L~ f)) .. f),((len f) -' 1))) by FINSEQ_5:6;
then (M1 /. 1) `2 = ((mid (f,((S-max (L~ f)) .. f),((len f) -' 1))) /. 1) `2 by FINSEQ_4:68
.= (f /. ((S-max (L~ f)) .. f)) `2 by A60, A370, SPRECT_2:8
.= (S-max (L~ f)) `2 by A369, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A379: M1 is_a_v.c._for f by A377, A378, SPRECT_2:def_3;
A380: L~ M1 = ((L~ M4) \/ (LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) \/ (L~ RB2) by A298, SPPOL_2:23
.= (L~ M4) \/ ((LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2)) by XBOOLE_1:4 ;
 len M1 >= 2 by TOPREAL1:def_8;
then  L~ M1 meets L~ M2 by A364, A379, A373, SPRECT_2:29;
then  L~ M2 meets (L~ RB2) \/ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(M4 /. (len M4)))) by A380, A362, XBOOLE_1:70;
then  L~ M2 meets L~ RB2 by A376, A363, XBOOLE_1:70;
then  L~ M2 meets L~ Red2 by A299, A365, XBOOLE_1:70;
then  L~ M2 meets L~ Red by A251, JORDAN3:41, XBOOLE_1:63;
hence  contradiction by A15, A245, A367, SPRECT_3:18, XBOOLE_1:63; ::_thesis: verum
end;
supposethat A381: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((N-min (L~ f)),(NE-corner (L~ f))) and
A382: N-min (L~ f) <> NW-corner (L~ f) ; ::_thesis: contradiction
set i1 = (S-min (L~ f)) .. f;
set i2 = (E-max (L~ f)) .. f;
A383: (S-min (L~ f)) .. f <= (W-min (L~ f)) .. f by A1, SPRECT_2:74;
 W-max (L~ f) <> N-min (L~ f) by A382, PSCOMP_1:61;
then  (S-min (L~ f)) .. f < (W-max (L~ f)) .. f by A1, A383, SPRECT_2:75, XXREAL_0:2;
then  ((S-min (L~ f)) .. f) + 1 <= (W-max (L~ f)) .. f by NAT_1:13;
then  ((S-min (L~ f)) .. f) + 1 < len f by A1, SPRECT_2:77, XXREAL_0:2;
then A384: (S-min (L~ f)) .. f < (len f) -' 1 by A61, XREAL_1:6;
A385: N-min (L~ f) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by RLTOPSP1:68;
A386: (N-min (L~ f)) `2 = (NW-corner (L~ f)) `2 by PSCOMP_1:37;
 (N-max (L~ f)) .. f > 1 by A1, SPRECT_2:69;
then A387: 1 < (E-max (L~ f)) .. f by A1, SPRECT_2:70, XXREAL_0:2;
 (E-max (L~ f)) .. f < (E-min (L~ f)) .. f by A1, SPRECT_2:71;
then  (E-max (L~ f)) .. f < (S-max (L~ f)) .. f by A1, SPRECT_2:72, XXREAL_0:2;
then A388: (E-max (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73, XXREAL_0:2;
then A389: 1 < (S-min (L~ f)) .. f by A387, XXREAL_0:2;
then reconsider M4 = mid (f,((S-min (L~ f)) .. f),((len f) -' 1)) as S-Sequence_in_R2 by A61, A384, JORDAN4:39;
A390: L~ M4 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A62, A257, A384, A389;
 (S-min (L~ f)) .. f < len f by A384, NAT_D:44;
then A391: (E-max (L~ f)) .. f < len f by A388, XXREAL_0:2;
then  ((E-max (L~ f)) .. f) + 1 <= len f by NAT_1:13;
then reconsider M3 = mid (f,1,((E-max (L~ f)) .. f)) as S-Sequence_in_R2 by A387, JORDAN4:39;
A392: L~ M3 misses L~ M4 by A62, A388, A384, A387, SPRECT_2:47;
 (E-max (L~ f)) .. f < (len f) -' 1 by A388, A384, XXREAL_0:2;
then A393: L~ M3 misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A105, A387;
A394: L~ M3 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A257, A387, A391;
A395: E-max (L~ f) in rng f by SPRECT_2:46;
then A396: (E-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then A397: M3 /. 1 = N-min (L~ f) by A1, A15, SPRECT_2:8;
A398: S-min (L~ f) in rng f by SPRECT_2:41;
then A399: (S-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then  L~ M4 misses L~ Red by A60, A245, SPRECT_3:18, XBOOLE_1:63;
then  L~ M4 misses L~ Red2 by A251, JORDAN3:41, XBOOLE_1:63;
then A400: L~ RB2 misses L~ M4 by A299, A390, XBOOLE_1:70;
A401: M4 /. (len M4) = f /. ((len f) -' 1) by A60, A399, SPRECT_2:9;
then  (LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) /\ (L~ M4) = {(M4 /. (len M4))} by A126, A384, A389;
then reconsider M1 = M4 ^ RB2 as S-Sequence_in_R2 by A78, A83, A96, A298, A300, A401, A400, SPRECT_3:21;
A402: L~ M1 = ((L~ M4) \/ (LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) \/ (L~ RB2) by A298, SPPOL_2:23
.= (L~ M4) \/ ((LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2)) by XBOOLE_1:4 ;
 1 in dom M3 by FINSEQ_5:6;
then  N-min (L~ f) in L~ M3 by A397, SPPOL_2:44;
then  N-min (L~ f) in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M3) by A385, XBOOLE_0:def_4;
then A403: {(N-min (L~ f))} c= (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M3) by ZFMISC_1:31;
A404: (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ f) = {(N-min (L~ f))} by PSCOMP_1:43;
then  (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M3) c= {(N-min (L~ f))} by A15, A396, SPRECT_3:18, XBOOLE_1:26;
then  (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M3) = {(N-min (L~ f))} by A403, XBOOLE_0:def_10;
then reconsider M2 = <*(NW-corner (L~ f))*> ^ M3 as S-Sequence_in_R2 by A382, A386, A397, SPRECT_3:16;
A405: (M2 /. 1) `1 = (NW-corner (L~ f)) `1 by FINSEQ_5:15
.= W-bound (L~ f) by EUCLID:52 ;
A406: now__::_thesis:_not_LSeg_((NW-corner_(L~_f)),(N-min_(L~_f)))_meets_L~_M4
assume  LSeg ((NW-corner (L~ f)),(N-min (L~ f))) meets L~ M4 ; ::_thesis: contradiction
then A407: (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M4) <> {} by XBOOLE_0:def_7;
 (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M4) c= {(N-min (L~ f))} by A60, A399, A404, SPRECT_3:18, XBOOLE_1:26;
then  (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M4) = {(N-min (L~ f))} by A407, ZFMISC_1:33;
then  N-min (L~ f) in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ M4) by TARSKI:def_1;
then  N-min (L~ f) in L~ M4 by XBOOLE_0:def_4;
hence  contradiction by A1, A62, A384, A389, SPRECT_3:30; ::_thesis: verum
end;
A408: (N-min (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
A409: (NE-corner (L~ f)) `2 = N-bound (L~ f) by EUCLID:52;
 mid (f,1,((E-max (L~ f)) .. f)) is_in_the_area_of f by A15, A396, SPRECT_2:23;
then A410: M2 is_in_the_area_of f by A63, SPRECT_2:24;
(M2 /. (len M2)) `1 = ((mid (f,1,((E-max (L~ f)) .. f))) /. (len (mid (f,1,((E-max (L~ f)) .. f))))) `1 by SPRECT_3:1
.= (f /. ((E-max (L~ f)) .. f)) `1 by A15, A396, SPRECT_2:9
.= (E-max (L~ f)) `1 by A395, FINSEQ_5:38
.= E-bound (L~ f) by EUCLID:52 ;
then A411: M2 is_a_h.c._for f by A410, A405, SPRECT_2:def_2;
A412: L~ M2 = (LSeg ((NW-corner (L~ f)),(M3 /. 1))) \/ (L~ M3) by SPPOL_2:20;
 mid (f,((S-min (L~ f)) .. f),((len f) -' 1)) is_in_the_area_of f by A60, A399, SPRECT_2:23;
then A413: M1 is_in_the_area_of f by A301, SPRECT_2:24;
A414: (M1 /. (len M1)) `2 = (Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))) `2 by A297, SPRECT_3:1
.= N-bound (L~ f) by A381, A409, A408, GOBOARD7:6 ;
 not mid (f,((S-min (L~ f)) .. f),((len f) -' 1)) is empty by A60, A399, SPRECT_2:7;
then  1 in dom (mid (f,((S-min (L~ f)) .. f),((len f) -' 1))) by FINSEQ_5:6;
then (M1 /. 1) `2 = ((mid (f,((S-min (L~ f)) .. f),((len f) -' 1))) /. 1) `2 by FINSEQ_4:68
.= (f /. ((S-min (L~ f)) .. f)) `2 by A60, A399, SPRECT_2:8
.= (S-min (L~ f)) `2 by A398, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A415: M1 is_a_v.c._for f by A413, A414, SPRECT_2:def_3;
A416: len M1 >= 2 by TOPREAL1:def_8;
now__::_thesis:_not_LSeg_((NW-corner_(L~_f)),(N-min_(L~_f)))_meets_L~_Red2
 NW-corner (L~ f) in LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by RLTOPSP1:68;
then  LSeg ((NW-corner (L~ f)),(N-min (L~ f))) c= LSeg ((NW-corner (L~ f)),(NE-corner (L~ f))) by A309, A310, TOPREAL1:6;
then  LSeg ((NW-corner (L~ f)),(N-min (L~ f))) c= L~ (SpStSeq (L~ f)) by A66, XBOOLE_1:1;
then A417: (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ Red2) c= {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A286, XBOOLE_1:26;
assume  LSeg ((NW-corner (L~ f)),(N-min (L~ f))) meets L~ Red2 ; ::_thesis: contradiction
then  (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ Red2) <> {} by XBOOLE_0:def_7;
then  (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ Red2) = {(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))} by A417, ZFMISC_1:33;
then  Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (L~ Red2) by TARSKI:def_1;
then  Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NW-corner (L~ f)),(N-min (L~ f))) by XBOOLE_0:def_4;
then A418: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (LSeg ((N-min (L~ f)),(NE-corner (L~ f)))) by A381, XBOOLE_0:def_4;
 (LSeg ((NW-corner (L~ f)),(N-min (L~ f)))) /\ (LSeg ((N-min (L~ f)),(NE-corner (L~ f)))) = {(N-min (L~ f))} by A309, A310, TOPREAL1:8;
then  Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) = N-min (L~ f) by A418, TARSKI:def_1;
hence  contradiction by A239, SPRECT_1:11; ::_thesis: verum
end;
then  LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses L~ RB2 by A256, A299, XBOOLE_1:70;
then  LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses (LSeg ((M4 /. (len M4)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2) by A132, A401, XBOOLE_1:70;
then A419: LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses L~ M1 by A402, A406, XBOOLE_1:70;
 len M2 >= 2 by TOPREAL1:def_8;
then A420: L~ M1 meets L~ M2 by A416, A415, A411, SPRECT_2:29;
 M3 /. 1 = f /. 1 by A15, A396, SPRECT_2:8;
then  L~ M3 meets L~ M1 by A1, A420, A419, A412, XBOOLE_1:70;
then  L~ M3 meets (L~ RB2) \/ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(M4 /. (len M4)))) by A402, A392, XBOOLE_1:70;
then  L~ M3 meets L~ RB2 by A401, A393, XBOOLE_1:70;
then  L~ M3 meets L~ Red2 by A299, A394, XBOOLE_1:70;
then  L~ M3 meets L~ Red by A251, JORDAN3:41, XBOOLE_1:63;
hence  contradiction by A15, A245, A396, SPRECT_3:18, XBOOLE_1:63; ::_thesis: verum
end;
supposethat A421: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))) and
A422: N-min (L~ f) = W-max (L~ f) ; ::_thesis: contradiction
A423: (RB2 /. 1) `1 = W-bound (L~ f) by A96, A298, A422, EUCLID:52;
A424: (SE-corner (L~ f)) `1 = E-bound (L~ f) by EUCLID:52;
 (NE-corner (L~ f)) `1 = E-bound (L~ f) by EUCLID:52;
then  (RB2 /. (len RB2)) `1 = E-bound (L~ f) by A297, A421, A424, GOBOARD7:5;
then A425: RB2 is_a_h.c._for f by A301, A423, SPRECT_2:def_2;
set i1 = (S-max (L~ f)) .. f;
set i2 = (N-max (L~ f)) .. f;
set i3 = (W-min (L~ f)) .. f;
A426: mid (f,((S-max (L~ f)) .. f),((N-max (L~ f)) .. f)) = Rev (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) by JORDAN4:18;
 (N-max (L~ f)) .. f <= (E-max (L~ f)) .. f by A1, SPRECT_2:70;
then  (N-max (L~ f)) .. f < (E-min (L~ f)) .. f by A1, SPRECT_2:71, XXREAL_0:2;
then A427: (N-max (L~ f)) .. f < (S-max (L~ f)) .. f by A1, SPRECT_2:72, XXREAL_0:2;
 W-min (L~ f) in rng f by SPRECT_2:43;
then  (W-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A428: (W-min (L~ f)) .. f <= len f by FINSEQ_3:25;
A429: 1 < (N-max (L~ f)) .. f by A1, SPRECT_2:69;
A430: S-max (L~ f) in rng f by SPRECT_2:42;
then A431: (S-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then  (S-max (L~ f)) .. f <= len f by FINSEQ_3:25;
then  mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f)) is S-Sequence_in_R2 by A429, A427, JORDAN4:40;
then reconsider M1 = mid (f,((S-max (L~ f)) .. f),((N-max (L~ f)) .. f)) as S-Sequence_in_R2 by A426;
A432: len RB2 >= 2 by TOPREAL1:def_8;
 (S-max (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73;
then  (W-min (L~ f)) .. f > (S-max (L~ f)) .. f by A1, SPRECT_2:74, XXREAL_0:2;
then  (S-max (L~ f)) .. f < len f by A428, XXREAL_0:2;
then  L~ (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A257, A429, A427;
then A433: L~ M1 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A426, SPPOL_2:22;
A434: N-max (L~ f) in rng f by SPRECT_2:40;
then A435: (N-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then A436: (M1 /. (len M1)) `2 = (f /. ((N-max (L~ f)) .. f)) `2 by A431, SPRECT_2:9
.= (N-max (L~ f)) `2 by A434, FINSEQ_5:38
.= N-bound (L~ f) by EUCLID:52 ;
A437: M1 is_in_the_area_of f by A431, A435, SPRECT_2:23;
(M1 /. 1) `2 = (f /. ((S-max (L~ f)) .. f)) `2 by A431, A435, SPRECT_2:8
.= (S-max (L~ f)) `2 by A430, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A438: M1 is_a_v.c._for f by A437, A436, SPRECT_2:def_3;
 len M1 >= 2 by TOPREAL1:def_8;
then  L~ M1 meets L~ RB2 by A432, A438, A425, SPRECT_2:29;
then  L~ M1 meets L~ Red2 by A299, A433, XBOOLE_1:70;
then  L~ M1 meets L~ Red by A251, JORDAN3:41, XBOOLE_1:63;
hence  contradiction by A245, A431, A435, SPRECT_3:18, XBOOLE_1:63; ::_thesis: verum
end;
supposethat A439: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((NE-corner (L~ f)),(SE-corner (L~ f))) and
A440: N-min (L~ f) <> W-max (L~ f) ; ::_thesis: contradiction
set i1 = (S-max (L~ f)) .. f;
set i2 = (N-max (L~ f)) .. f;
set i3 = (W-min (L~ f)) .. f;
 (W-max (L~ f)) .. f <= (len f) -' 1 by A1, NAT_D:49, SPRECT_2:77;
then A441: (W-min (L~ f)) .. f < (len f) -' 1 by A1, A440, SPRECT_2:75, XXREAL_0:2;
A442: W-min (L~ f) in rng f by SPRECT_2:43;
then A443: (W-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A444: 1 <= (W-min (L~ f)) .. f by FINSEQ_3:25;
then reconsider M3 = mid (f,((W-min (L~ f)) .. f),((len f) -' 1)) as S-Sequence_in_R2 by A61, A441, JORDAN4:39;
 L~ M3 misses L~ Red by A60, A245, A443, SPRECT_3:18, XBOOLE_1:63;
then A445: L~ M3 misses L~ Red2 by A251, JORDAN3:41, XBOOLE_1:63;
 L~ M3 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A62, A257, A441, A444;
then A446: L~ RB2 misses L~ M3 by A299, A445, XBOOLE_1:70;
A447: M3 /. (len M3) = f /. ((len f) -' 1) by A60, A443, SPRECT_2:9;
then  (LSeg ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) /\ (L~ M3) = {(M3 /. (len M3))} by A126, A441, A444;
then reconsider M2 = M3 ^ RB2 as S-Sequence_in_R2 by A78, A83, A96, A298, A300, A447, A446, SPRECT_3:21;
 mid (f,((W-min (L~ f)) .. f),((len f) -' 1)) is_in_the_area_of f by A60, A443, SPRECT_2:23;
then A448: M2 is_in_the_area_of f by A301, SPRECT_2:24;
A449: mid (f,((S-max (L~ f)) .. f),((N-max (L~ f)) .. f)) = Rev (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) by JORDAN4:18;
A450: 1 < (N-max (L~ f)) .. f by A1, SPRECT_2:69;
 (N-max (L~ f)) .. f <= (E-max (L~ f)) .. f by A1, SPRECT_2:70;
then  (N-max (L~ f)) .. f < (E-min (L~ f)) .. f by A1, SPRECT_2:71, XXREAL_0:2;
then A451: (N-max (L~ f)) .. f < (S-max (L~ f)) .. f by A1, SPRECT_2:72, XXREAL_0:2;
A452: S-max (L~ f) in rng f by SPRECT_2:42;
then A453: (S-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then  (S-max (L~ f)) .. f <= len f by FINSEQ_3:25;
then  mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f)) is S-Sequence_in_R2 by A450, A451, JORDAN4:40;
then reconsider M1 = mid (f,((S-max (L~ f)) .. f),((N-max (L~ f)) .. f)) as S-Sequence_in_R2 by A449;
 (S-max (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73;
then A454: (W-min (L~ f)) .. f > (S-max (L~ f)) .. f by A1, SPRECT_2:74, XXREAL_0:2;
then A455: L~ M1 misses L~ M3 by A62, A450, A451, A441, SPRECT_2:50;
 (W-min (L~ f)) .. f < len f by A61, A441, NAT_1:13;
then  (S-max (L~ f)) .. f < len f by A454, XXREAL_0:2;
then  L~ (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A257, A450, A451;
then A456: L~ M1 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))) by A449, SPPOL_2:22;
A457: len M1 >= 2 by TOPREAL1:def_8;
A458: N-max (L~ f) in rng f by SPRECT_2:40;
then A459: (N-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then A460: (M1 /. (len M1)) `2 = (f /. ((N-max (L~ f)) .. f)) `2 by A453, SPRECT_2:9
.= (N-max (L~ f)) `2 by A458, FINSEQ_5:38
.= N-bound (L~ f) by EUCLID:52 ;
 (S-max (L~ f)) .. f < (len f) -' 1 by A454, A441, XXREAL_0:2;
then  L~ (mid (f,((N-max (L~ f)) .. f),((S-max (L~ f)) .. f))) misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A105, A450, A451;
then A461: L~ M1 misses LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(f /. ((len f) -' 1))) by A449, SPPOL_2:22;
A462: (SE-corner (L~ f)) `1 = E-bound (L~ f) by EUCLID:52;
A463: (NE-corner (L~ f)) `1 = E-bound (L~ f) by EUCLID:52;
A464: (M2 /. (len M2)) `1 = (RB2 /. (len RB2)) `1 by SPRECT_3:1
.= E-bound (L~ f) by A297, A439, A463, A462, GOBOARD7:5 ;
 not mid (f,((W-min (L~ f)) .. f),((len f) -' 1)) is empty by A60, A443, SPRECT_2:7;
then  1 in dom (mid (f,((W-min (L~ f)) .. f),((len f) -' 1))) by FINSEQ_5:6;
then (M2 /. 1) `1 = ((mid (f,((W-min (L~ f)) .. f),((len f) -' 1))) /. 1) `1 by FINSEQ_4:68
.= (f /. ((W-min (L~ f)) .. f)) `1 by A60, A443, SPRECT_2:8
.= (W-min (L~ f)) `1 by A442, FINSEQ_5:38
.= W-bound (L~ f) by EUCLID:52 ;
then A465: M2 is_a_h.c._for f by A448, A464, SPRECT_2:def_2;
A466: L~ M2 = ((L~ M3) \/ (LSeg ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f))))))))) \/ (L~ RB2) by A298, SPPOL_2:23
.= (L~ M3) \/ ((LSeg ((M3 /. (len M3)),((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))))) \/ (L~ RB2)) by XBOOLE_1:4 ;
A467: M1 is_in_the_area_of f by A453, A459, SPRECT_2:23;
(M1 /. 1) `2 = (f /. ((S-max (L~ f)) .. f)) `2 by A453, A459, SPRECT_2:8
.= (S-max (L~ f)) `2 by A452, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A468: M1 is_a_v.c._for f by A467, A460, SPRECT_2:def_3;
 len M2 >= 2 by TOPREAL1:def_8;
then  L~ M1 meets L~ M2 by A457, A468, A465, SPRECT_2:29;
then  L~ M1 meets (L~ RB2) \/ (LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * (i,(width (GoB f)))))),(M3 /. (len M3)))) by A466, A455, XBOOLE_1:70;
then  L~ M1 meets L~ RB2 by A447, A461, XBOOLE_1:70;
then  L~ M1 meets L~ Red2 by A299, A456, XBOOLE_1:70;
then  L~ M1 meets L~ Red by A251, JORDAN3:41, XBOOLE_1:63;
hence  contradiction by A245, A453, A459, SPRECT_3:18, XBOOLE_1:63; ::_thesis: verum
end;
supposeA469: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((SE-corner (L~ f)),(SW-corner (L~ f))) ; ::_thesis: contradiction
A470: (SW-corner (L~ f)) `2 = S-bound (L~ f) by EUCLID:52;
 (SE-corner (L~ f)) `2 = S-bound (L~ f) by EUCLID:52;
then  (RB1 /. 1) `2 = S-bound (L~ f) by A302, A469, A470, GOBOARD7:6;
then A471: RB1 is_a_v.c._for f by A170, A303, A306, SPRECT_2:def_3;
A472: len RB1 >= 2 by TOPREAL1:def_8;
set i1 = (E-min (L~ f)) .. f;
set i2 = (W-min (L~ f)) .. f;
A473: mid (f,((W-min (L~ f)) .. f),((E-min (L~ f)) .. f)) = Rev (mid (f,((E-min (L~ f)) .. f),((W-min (L~ f)) .. f))) by JORDAN4:18;
 (E-min (L~ f)) .. f <= (S-max (L~ f)) .. f by A1, SPRECT_2:72;
then  (E-min (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73, XXREAL_0:2;
then A474: (E-min (L~ f)) .. f < (W-min (L~ f)) .. f by A1, SPRECT_2:74, XXREAL_0:2;
 (N-max (L~ f)) .. f > 1 by A1, SPRECT_2:69;
then  (E-max (L~ f)) .. f > 1 by A1, SPRECT_2:70, XXREAL_0:2;
then A475: 1 < (E-min (L~ f)) .. f by A1, SPRECT_2:71, XXREAL_0:2;
A476: W-min (L~ f) in rng f by SPRECT_2:43;
then A477: (W-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A478: (W-min (L~ f)) .. f <= len f by FINSEQ_3:25;
then  mid (f,((E-min (L~ f)) .. f),((W-min (L~ f)) .. f)) is S-Sequence_in_R2 by A475, A474, JORDAN4:40;
then reconsider M2 = mid (f,((W-min (L~ f)) .. f),((E-min (L~ f)) .. f)) as S-Sequence_in_R2 by A473;
 L~ (mid (f,((E-min (L~ f)) .. f),((W-min (L~ f)) .. f))) misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A270, A475, A474, A478;
then A479: L~ M2 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A473, SPPOL_2:22;
A480: E-min (L~ f) in rng f by SPRECT_2:45;
then A481: (E-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A482: M2 is_in_the_area_of f by A477, SPRECT_2:23;
A483: (M2 /. 1) `1 = (f /. ((W-min (L~ f)) .. f)) `1 by A481, A477, SPRECT_2:8
.= (W-min (L~ f)) `1 by A476, FINSEQ_5:38
.= W-bound (L~ f) by EUCLID:52 ;
(M2 /. (len M2)) `1 = (f /. ((E-min (L~ f)) .. f)) `1 by A481, A477, SPRECT_2:9
.= (E-min (L~ f)) `1 by A480, FINSEQ_5:38
.= E-bound (L~ f) by EUCLID:52 ;
then A484: M2 is_a_h.c._for f by A482, A483, SPRECT_2:def_2;
 len M2 >= 2 by TOPREAL1:def_8;
then  L~ RB1 meets L~ M2 by A472, A471, A484, SPRECT_2:29;
then  L~ M2 meets L~ Red1 by A304, A479, XBOOLE_1:70;
then  L~ M2 meets L~ Red by A264, JORDAN3:41, XBOOLE_1:63;
hence  contradiction by A245, A481, A477, SPRECT_3:18, XBOOLE_1:63; ::_thesis: verum
end;
supposeA485: Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))) in LSeg ((SW-corner (L~ f)),(NW-corner (L~ f))) ; ::_thesis: contradiction
A486: (SW-corner (L~ f)) `1 = W-bound (L~ f) by EUCLID:52;
set i1 = (S-min (L~ f)) .. f;
set i3 = (E-min (L~ f)) .. f;
A487: (NW-corner (L~ f)) `1 = W-bound (L~ f) by EUCLID:52;
 (N-max (L~ f)) .. f > 1 by A1, SPRECT_2:69;
then  (E-max (L~ f)) .. f > 1 by A1, SPRECT_2:70, XXREAL_0:2;
then  (E-max (L~ f)) .. f >= 1 + 1 by NAT_1:13;
then A488: 2 < (E-min (L~ f)) .. f by A1, SPRECT_2:71, XXREAL_0:2;
A489: E-min (L~ f) in rng f by SPRECT_2:45;
then A490: (E-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A491: (E-min (L~ f)) .. f <= len f by FINSEQ_3:25;
then reconsider M3 = mid (f,2,((E-min (L~ f)) .. f)) as S-Sequence_in_R2 by A488, JORDAN4:40;
 L~ M3 misses L~ Red by A57, A245, A490, SPRECT_3:18, XBOOLE_1:63;
then A492: L~ M3 misses L~ Red1 by A264, JORDAN3:41, XBOOLE_1:63;
 L~ M3 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A270, A488, A491;
then A493: L~ RB1 misses L~ M3 by A304, A492, XBOOLE_1:70;
A494: M3 /. 1 = f /. 2 by A57, A490, SPRECT_2:8;
then  (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(M3 /. 1))) /\ (L~ M3) = {(M3 /. 1)} by A191, A488, A491;
then reconsider M2 = RB1 ^ M3 as S-Sequence_in_R2 by A80, A170, A303, A305, A494, A493, SPRECT_3:21;
A495: (M2 /. (len M2)) `1 = ((mid (f,2,((E-min (L~ f)) .. f))) /. (len (mid (f,2,((E-min (L~ f)) .. f))))) `1 by SPRECT_3:1
.= (f /. ((E-min (L~ f)) .. f)) `1 by A57, A490, SPRECT_2:9
.= (E-min (L~ f)) `1 by A489, FINSEQ_5:38
.= E-bound (L~ f) by EUCLID:52 ;
 mid (f,2,((E-min (L~ f)) .. f)) is_in_the_area_of f by A57, A490, SPRECT_2:23;
then A496: M2 is_in_the_area_of f by A306, SPRECT_2:24;
 1 in dom RB1 by FINSEQ_5:6;
then (M2 /. 1) `1 = (RB1 /. 1) `1 by FINSEQ_4:68
.= W-bound (L~ f) by A302, A485, A487, A486, GOBOARD7:5 ;
then A497: M2 is_a_h.c._for f by A496, A495, SPRECT_2:def_2;
A498: L~ M2 = ((L~ RB1) \/ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(M3 /. 1)))) \/ (L~ M3) by A303, SPPOL_2:23;
 (W-min (L~ f)) .. f < len f by A1, SPRECT_2:76;
then A499: (S-min (L~ f)) .. f < len f by A1, SPRECT_2:74, XXREAL_0:2;
 (E-min (L~ f)) .. f <= (S-max (L~ f)) .. f by A1, SPRECT_2:72;
then A500: (E-min (L~ f)) .. f < (S-min (L~ f)) .. f by A1, SPRECT_2:73, XXREAL_0:2;
then A501: 2 < (S-min (L~ f)) .. f by A488, XXREAL_0:2;
then A502: 1 < (S-min (L~ f)) .. f by XXREAL_0:2;
then reconsider M1 = mid (f,((S-min (L~ f)) .. f),(len f)) as S-Sequence_in_R2 by A499, JORDAN4:40;
A503: L~ M1 misses L~ M3 by A500, A499, A488, SPRECT_2:47;
A504: L~ M1 misses LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(f /. 2)) by A173, A499, A501;
A505: S-min (L~ f) in rng f by SPRECT_2:41;
then A506: (S-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A507: M1 is_in_the_area_of f by A58, SPRECT_2:23;
A508: (M1 /. (len M1)) `2 = (f /. (len f)) `2 by A58, A506, SPRECT_2:9
.= (f /. 1) `2 by FINSEQ_6:def_1
.= N-bound (L~ f) by A1, EUCLID:52 ;
(M1 /. 1) `2 = (f /. ((S-min (L~ f)) .. f)) `2 by A58, A506, SPRECT_2:8
.= (S-min (L~ f)) `2 by A505, FINSEQ_5:38
.= S-bound (L~ f) by EUCLID:52 ;
then A509: M1 is_a_v.c._for f by A507, A508, SPRECT_2:def_3;
A510: L~ M1 misses LSeg ((First_Point ((L~ (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f)))))))),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. 1),((L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))) /. (len (L_Cut (Red9,(Last_Point ((L~ Red9),(Red9 /. 1),(Red9 /. (len Red9)),(L~ (SpStSeq (L~ f))))))))),(LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))))))),((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))) by A270, A499, A502;
A511: len M1 >= 2 by TOPREAL1:def_8;
 len M2 >= 2 by TOPREAL1:def_8;
then  L~ M1 meets L~ M2 by A511, A509, A497, SPRECT_2:29;
then  L~ M1 meets (L~ RB1) \/ (LSeg (((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(M3 /. 1))) by A498, A503, XBOOLE_1:70;
then  L~ M1 meets L~ RB1 by A494, A504, XBOOLE_1:70;
then  L~ M1 meets L~ Red1 by A304, A510, XBOOLE_1:70;
then  L~ M1 meets L~ Red by A264, JORDAN3:41, XBOOLE_1:63;
hence  contradiction by A58, A245, A506, SPRECT_3:18, XBOOLE_1:63; ::_thesis: verum
end;
end;
end;

Lm2:  for f being non constant standard special_circular_sequence st f /. 1 = N-min (L~ f) holds
LeftComp f <> RightComp f
proof
let f be non constant standard special_circular_sequence; ::_thesis: ( f /. 1 = N-min (L~ f) implies LeftComp f <> RightComp f )
assume A1: f /. 1 = N-min (L~ f) ; ::_thesis: LeftComp f <> RightComp f
percases ( f is clockwise_oriented or Rev f is clockwise_oriented ) by REVROT_1:38;
suppose f is clockwise_oriented ; ::_thesis: LeftComp f <> RightComp f
hence  LeftComp f <> RightComp f by A1, Lm1; ::_thesis: verum
end;
supposeA2: Rev f is clockwise_oriented ; ::_thesis: LeftComp f <> RightComp f
A3: LeftComp (Rev f) = RightComp f by GOBOARD9:23;
A4: RightComp (Rev f) = LeftComp f by GOBOARD9:24;
N-min (L~ (Rev f)) = N-min (L~ f) by SPPOL_2:22
.= (Rev f) /. (len f) by A1, FINSEQ_5:65
.= (Rev f) /. (len (Rev f)) by FINSEQ_5:def_3
.= (Rev f) /. 1 by FINSEQ_6:def_1 ;
hence  LeftComp f <> RightComp f by A2, A3, A4, Lm1; ::_thesis: verum
end;
end;
end;

theorem :: SPRECT_4:6
for f being non constant standard special_circular_sequence holds LeftComp f <> RightComp f
proof
let f be non constant standard special_circular_sequence; ::_thesis: LeftComp f <> RightComp f
set g = Rotate (f,(N-min (L~ f)));
A1: L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33;
 N-min (L~ f) in rng f by SPRECT_2:39;
then A2: (Rotate (f,(N-min (L~ f)))) /. 1 = N-min (L~ (Rotate (f,(N-min (L~ f))))) by A1, FINSEQ_6:92;
A3: RightComp (Rotate (f,(N-min (L~ f)))) = RightComp f by REVROT_1:37;
 LeftComp (Rotate (f,(N-min (L~ f)))) = LeftComp f by REVROT_1:36;
hence  LeftComp f <> RightComp f by A2, A3, Lm2; ::_thesis: verum
end;