:: SPRECT_4 semantic presentation

registration

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

end;

theorem Th1: :: SPRECT_4:1

for b₁ being S-Sequence_in_R2
for b₂ being closed Subset of (TOP-REAL 2) st L~ b₁ meets b₂ & not b₁ /. 1 in b₂ holds
(L~ (R_Cut b₁,(First_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂))) /\ b₂ = {(First_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂)}

proof end;

theorem Th2: :: SPRECT_4:2

for b₁ being non empty FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₁ is_S-Seq & b₂ = b₁ /. (len b₁) holds
L~ (L_Cut b₁,b₂) = {}

proof end;

theorem Th3: :: SPRECT_4:3

canceled;

theorem Th4: :: SPRECT_4:4

for b₁ being S-Sequence_in_R2
for b₂ being Point of (TOP-REAL 2)
for b₃ being Nat st 1 <= b₃ & b₃ < len b₁ & b₂ in L~ (mid b₁,b₃,(len b₁)) holds
LE b₁ /. b₃,b₂, L~ b₁,b₁ /. 1,b₁ /. (len b₁)

proof end;

theorem Th5: :: SPRECT_4:5

for b₁ being S-Sequence_in_R2
for b₂, b₃ being Point of (TOP-REAL 2)
for b₄ being Nat st 1 <= b₄ & b₄ < len b₁ & b₂ in LSeg b₁,b₄ & b₃ in LSeg b₂,(b₁ /. (b₄ + 1)) holds
LE b₂,b₃, L~ b₁,b₁ /. 1,b₁ /. (len b₁)

proof end;

theorem Th6: :: SPRECT_4:6

for b₁ being S-Sequence_in_R2
for b₂ being closed Subset of (TOP-REAL 2) st L~ b₁ meets b₂ & not b₁ /. (len b₁) in b₂ holds
(L~ (L_Cut b₁,(Last_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂))) /\ b₂ = {(Last_Point (L~ b₁),(b₁ /. 1),(b₁ /. (len b₁)),b₂)}

proof end;

Lemma5: for b₁ being clockwise_oriented non constant standard special_circular_sequence st b₁ /. 1 = N-min (L~ b₁) holds
LeftComp b₁ <> RightComp b₁

proof end;

Lemma6: for b₁ being non constant standard special_circular_sequence st b₁ /. 1 = N-min (L~ b₁) holds
LeftComp b₁ <> RightComp b₁

proof end;

theorem Th7: :: SPRECT_4:7

for b₁ being non constant standard special_circular_sequence holds LeftComp b₁ <> RightComp b₁

proof end;