begin
begin
theorem Th8:
for
P being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) for
g being
Function of
I[01],
((TOP-REAL 2) | P) for
s1,
s2 being
Real st
P is_an_arc_of p1,
p2 &
g is
being_homeomorphism &
g . 0 = p1 &
g . 1
= p2 &
g . s1 = q1 &
0 <= s1 &
s1 <= 1 &
g . s2 = q2 &
0 <= s2 &
s2 <= 1 &
s1 <= s2 holds
LE q1,
q2,
P,
p1,
p2
theorem Th10:
for
P being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 &
q1 in P holds
(
LE p1,
q1,
P,
p1,
p2 &
LE q1,
p2,
P,
p1,
p2 )
theorem Th12:
for
P being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 &
LE q1,
q2,
P,
p1,
p2 &
LE q2,
q1,
P,
p1,
p2 holds
q1 = q2
theorem Th13:
for
P being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2,
q3 being
Point of
(TOP-REAL 2) st
LE q1,
q2,
P,
p1,
p2 &
LE q2,
q3,
P,
p1,
p2 holds
LE q1,
q3,
P,
p1,
p2
theorem
for
P being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 &
q1 in P &
q2 in P &
q1 <> q2 & not (
LE q1,
q2,
P,
p1,
p2 & not
LE q2,
q1,
P,
p1,
p2 ) holds
(
LE q2,
q1,
P,
p1,
p2 & not
LE q1,
q2,
P,
p1,
p2 )
begin
theorem Th17:
for
q1,
q2,
p1,
p2 being
Point of
(TOP-REAL 2) st
p1 <> p2 &
LE q1,
q2,
LSeg (
p1,
p2),
p1,
p2 holds
LE q1,
q2,
p1,
p2
theorem
for
P,
Q being
Subset of
(TOP-REAL 2) for
p1,
p2 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 &
P meets Q &
P /\ Q is
closed holds
(
First_Point (
P,
p1,
p2,
Q)
= Last_Point (
P,
p2,
p1,
Q) &
Last_Point (
P,
p1,
p2,
Q)
= First_Point (
P,
p2,
p1,
Q) )
theorem Th19:
for
f being
FinSequence of
(TOP-REAL 2) for
Q being
Subset of
(TOP-REAL 2) for
i being
Element of
NAT st
L~ f meets Q &
Q is
closed &
f is
being_S-Seq & 1
<= i &
i + 1
<= len f &
First_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
in LSeg (
f,
i) holds
First_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
= First_Point (
(LSeg (f,i)),
(f /. i),
(f /. (i + 1)),
Q)
theorem Th20:
for
f being
FinSequence of
(TOP-REAL 2) for
Q being
Subset of
(TOP-REAL 2) for
i being
Element of
NAT st
L~ f meets Q &
Q is
closed &
f is
being_S-Seq & 1
<= i &
i + 1
<= len f &
Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
in LSeg (
f,
i) holds
Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
= Last_Point (
(LSeg (f,i)),
(f /. i),
(f /. (i + 1)),
Q)
Lm1:
for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1)
Lm2:
for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1)
Lm3:
for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1)
Lm4:
for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1)
theorem
for
f being
FinSequence of
(TOP-REAL 2) for
Q being
Subset of
(TOP-REAL 2) for
q being
Point of
(TOP-REAL 2) for
i,
j being
Element of
NAT st
L~ f meets Q &
f is
being_S-Seq &
Q is
closed &
First_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
in LSeg (
f,
i) & 1
<= i &
i + 1
<= len f &
q in LSeg (
f,
j) & 1
<= j &
j + 1
<= len f &
q in Q &
First_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
<> q holds
(
i <= j & (
i = j implies
LE First_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q),
q,
f /. i,
f /. (i + 1) ) )
theorem
for
f being
FinSequence of
(TOP-REAL 2) for
Q being
Subset of
(TOP-REAL 2) for
q being
Point of
(TOP-REAL 2) for
i,
j being
Element of
NAT st
L~ f meets Q &
f is
being_S-Seq &
Q is
closed &
Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
in LSeg (
f,
i) & 1
<= i &
i + 1
<= len f &
q in LSeg (
f,
j) & 1
<= j &
j + 1
<= len f &
q in Q &
Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
<> q holds
(
i >= j & (
i = j implies
LE q,
Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q),
f /. i,
f /. (i + 1) ) )
theorem Th29:
for
f being
FinSequence of
(TOP-REAL 2) for
q1,
q2 being
Point of
(TOP-REAL 2) for
i being
Element of
NAT st
q1 in LSeg (
f,
i) &
q2 in LSeg (
f,
i) &
f is
being_S-Seq & 1
<= i &
i + 1
<= len f &
LE q1,
q2,
L~ f,
f /. 1,
f /. (len f) holds
LE q1,
q2,
LSeg (
f,
i),
f /. i,
f /. (i + 1)
theorem
for
f being
FinSequence of
(TOP-REAL 2) for
q1,
q2 being
Point of
(TOP-REAL 2) st
q1 in L~ f &
q2 in L~ f &
f is
being_S-Seq &
q1 <> q2 holds
(
LE q1,
q2,
L~ f,
f /. 1,
f /. (len f) iff for
i,
j being
Element of
NAT st
q1 in LSeg (
f,
i) &
q2 in LSeg (
f,
j) & 1
<= i &
i + 1
<= len f & 1
<= j &
j + 1
<= len f holds
(
i <= j & (
i = j implies
LE q1,
q2,
f /. i,
f /. (i + 1) ) ) )