begin
theorem
canceled;
theorem
for
a,
b,
c,
X being
set st
a in X &
b in X &
c in X holds
{a,b,c} c= X
theorem
canceled;
theorem
theorem Th5:
theorem
canceled;
theorem Th7:
theorem Th8:
theorem Th9:
for
A being
Subset of
for
q1,
q2,
p1,
p2 being
Point of 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
for
p1,
p2,
q1,
q2 being
Point of 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
for
p1,
p2,
q1,
q2 being
Point of 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
for
q1,
q2,
p1,
p2 being
Point of st
LE q1,
q2,
A,
p1,
p2 holds
not
Segment A,
p1,
p2,
q1,
q2 is
empty
theorem
:: deftheorem JORDAN16:def 1 :
canceled;
:: deftheorem JORDAN16:def 2 :
canceled;
:: deftheorem Def3 defines AffineMap JORDAN16:def 3 :
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem
theorem Th30:
theorem
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
for
A being
Subset of
for
p1,
p2,
q1,
q2 being
Point of 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