begin
theorem
theorem Th5:
theorem Th7:
theorem Th8:
theorem Th9:
for
A being
Subset of
(TOP-REAL 2) for
q1,
q2,
p1,
p2 being
Point of
(TOP-REAL 2) st
LE q1,
q2,
A,
p1,
p2 holds
(
q1 in Segment (
A,
p1,
p2,
q1,
q2) &
q2 in Segment (
A,
p1,
p2,
q1,
q2) )
theorem
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem
theorem
theorem Th19:
theorem Th20:
for
A being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
A is_an_arc_of p1,
p2 &
LE q1,
q2,
A,
p1,
p2 holds
ex
g being
Function of
I[01],
((TOP-REAL 2) | A) ex
s1,
s2 being
Real st
(
g is
being_homeomorphism &
g . 0 = p1 &
g . 1
= p2 &
g . s1 = q1 &
g . s2 = q2 &
0 <= s1 &
s1 <= s2 &
s2 <= 1 )
theorem Th21:
for
A being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
A is_an_arc_of p1,
p2 &
LE q1,
q2,
A,
p1,
p2 &
q1 <> q2 holds
ex
g being
Function of
I[01],
((TOP-REAL 2) | A) ex
s1,
s2 being
Real st
(
g is
being_homeomorphism &
g . 0 = p1 &
g . 1
= p2 &
g . s1 = q1 &
g . s2 = q2 &
0 <= s1 &
s1 < s2 &
s2 <= 1 )
theorem
for
A being
Subset of
(TOP-REAL 2) for
q1,
q2,
p1,
p2 being
Point of
(TOP-REAL 2) st
LE q1,
q2,
A,
p1,
p2 holds
not
Segment (
A,
p1,
p2,
q1,
q2) is
empty
theorem
theorem Th35:
theorem Th36:
for
A being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
A is_an_arc_of p1,
p2 &
LE q1,
q2,
A,
p1,
p2 &
q1 <> q2 holds
Segment (
A,
p1,
p2,
q1,
q2)
is_an_arc_of q1,
q2
theorem
theorem
theorem