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 I[01] holds P is Real
theorem Th7:
theorem
begin
theorem Th9:
theorem Th10:
theorem Th11:
theorem
for
p1,
p2,
q1,
q2,
q3 being
Point of
(TOP-REAL 2) st
p1 <> p2 &
LE q1,
q2,
p1,
p2 &
LE q2,
q3,
p1,
p2 holds
LE q1,
q3,
p1,
p2
theorem
theorem
theorem
begin
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th22:
theorem
theorem Th24:
Lm3:
for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) 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 (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) 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
(TOP-REAL 2) for
p,
q being
Point of
(TOP-REAL 2) 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;