begin
theorem Th1:
for
i1 being
Nat st 1
<= i1 holds
i1 -' 1
< i1
theorem
for
i,
k being
Nat st
i + 1
<= k holds
1
<= k -' i
theorem
for
i,
k being
Nat st 1
<= i & 1
<= k holds
(k -' i) + 1
<= k
Lm1:
for r being real number st 0 <= r & r <= 1 holds
( 0 <= 1 - r & 1 - r <= 1 )
theorem
theorem
theorem
Lm2:
for P being Point of holds P is Real
theorem Th7:
theorem
begin
theorem Th9:
for
p1,
p2,
p being
Point of st
p1 <> p2 &
p in LSeg p1,
p2 holds
LE p,
p,
p1,
p2
theorem Th10:
for
p,
p1,
p2 being
Point of st
p1 <> p2 &
p in LSeg p1,
p2 holds
LE p1,
p,
p1,
p2
theorem Th11:
for
p,
p1,
p2 being
Point of st
p in LSeg p1,
p2 &
p1 <> p2 holds
LE p,
p2,
p1,
p2
theorem
for
p1,
p2,
q1,
q2,
q3 being
Point of st
p1 <> p2 &
LE q1,
q2,
p1,
p2 &
LE q2,
q3,
p1,
p2 holds
LE q1,
q3,
p1,
p2
theorem
for
p,
q being
Point of st
p <> q holds
LSeg p,
q = { p1 where p1 is Point of : ( LE p,p1,p,q & LE p1,q,p,q ) }
theorem
theorem
begin
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th22:
theorem
theorem Th24:
Lm3:
for f being FinSequence of
for p, q being Point of st p in L~ f & q in L~ f & p <> f . (len f) & f is being_S-Seq & not p in L~ (L_Cut f,q) holds
q in L~ (L_Cut f,p)
theorem Th25:
theorem
Lm4:
for f being FinSequence of
for p, q being Point of st p in L~ f & q in L~ f & ( Index p,f < Index q,f or ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ) & p <> q holds
L~ (B_Cut f,p,q) c= L~ f
theorem
theorem
theorem
theorem Th30:
theorem
theorem
theorem
theorem
theorem
theorem
for
f being
FinSequence of
for
p,
q being
Point of st
p in L~ f &
q in L~ f & (
Index p,
f < Index q,
f or (
Index p,
f = Index q,
f &
LE p,
q,
f /. (Index p,f),
f /. ((Index p,f) + 1) ) ) &
p <> q holds
L~ (B_Cut f,p,q) c= L~ f by Lm4;