:: by Andrzej Trybulec and Yatsuka Nakamura

::

:: Received January 21, 1999

:: Copyright (c) 1999-2016 Association of Mizar Users

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))}

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 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)) = {}

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 end;

theorem Th3: :: SPRECT_4:3

for f being S-Sequence_in_R2

for p being Point of (TOP-REAL 2)

for j being 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)

for p being Point of (TOP-REAL 2)

for j being 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 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 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)

for p, q being Point of (TOP-REAL 2)

for j being 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 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))}

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 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 end;

Lm2: for f being non constant standard special_circular_sequence st f /. 1 = N-min (L~ f) holds

LeftComp f <> RightComp f

proof end;