:: SPRECT_4 semantic presentation

registration

let T be non empty being_T2 TopSpace;
cluster compact -> closed Element of K40(the carrier of T);
coherence by COMPTS_1:16;

end;

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 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_S-Seq & p = f /. (len f) holds
L~ (L_Cut f,p) = {}

proof end;

theorem :: SPRECT_4:3

canceled;

theorem Th4: :: SPRECT_4:4

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)

proof end;

theorem Th5: :: SPRECT_4:5

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)

proof end;

theorem Th6: :: SPRECT_4:6

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

Lm1: for f being clockwise_oriented non constant standard 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;

theorem :: SPRECT_4:7

for f being non constant standard special_circular_sequence holds LeftComp f <> RightComp f

proof end;