begin
theorem Th8:
for
p,
q being
Point of
(TOP-REAL 2) for
f being
FinSequence of
(TOP-REAL 2) for
r being
Real for
u being
Point of
(Euclid 2) st
p `1 <> q `1 &
p `2 <> q `2 &
p in Ball (
u,
r) &
q in Ball (
u,
r) &
|[(p `1),(q `2)]| in Ball (
u,
r) &
f = <*p,|[(p `1),(q `2)]|,q*> holds
(
f is
being_S-Seq &
f /. 1
= p &
f /. (len f) = q &
L~ f is_S-P_arc_joining p,
q &
L~ f c= Ball (
u,
r) )
theorem Th9:
for
p,
q being
Point of
(TOP-REAL 2) for
f being
FinSequence of
(TOP-REAL 2) for
r being
Real for
u being
Point of
(Euclid 2) st
p `1 <> q `1 &
p `2 <> q `2 &
p in Ball (
u,
r) &
q in Ball (
u,
r) &
|[(q `1),(p `2)]| in Ball (
u,
r) &
f = <*p,|[(q `1),(p `2)]|,q*> holds
(
f is
being_S-Seq &
f /. 1
= p &
f /. (len f) = q &
L~ f is_S-P_arc_joining p,
q &
L~ f c= Ball (
u,
r) )
theorem Th20:
for
p being
Point of
(TOP-REAL 2) for
f,
h being
FinSequence of
(TOP-REAL 2) for
r being
Real for
u being
Point of
(Euclid 2) st
f /. (len f) in Ball (
u,
r) &
p in Ball (
u,
r) &
|[(p `1),((f /. (len f)) `2)]| in Ball (
u,
r) &
f is
being_S-Seq &
p `1 <> (f /. (len f)) `1 &
p `2 <> (f /. (len f)) `2 &
h = f ^ <*|[(p `1),((f /. (len f)) `2)]|,p*> &
((LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) \/ (LSeg (|[(p `1),((f /. (len f)) `2)]|,p))) /\ (L~ f) = {(f /. (len f))} holds
(
L~ h is_S-P_arc_joining f /. 1,
p &
L~ h c= (L~ f) \/ (Ball (u,r)) )
theorem Th21:
for
p being
Point of
(TOP-REAL 2) for
f,
h being
FinSequence of
(TOP-REAL 2) for
r being
Real for
u being
Point of
(Euclid 2) st
f /. (len f) in Ball (
u,
r) &
p in Ball (
u,
r) &
|[((f /. (len f)) `1),(p `2)]| in Ball (
u,
r) &
f is
being_S-Seq &
p `1 <> (f /. (len f)) `1 &
p `2 <> (f /. (len f)) `2 &
h = f ^ <*|[((f /. (len f)) `1),(p `2)]|,p*> &
((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) \/ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p))) /\ (L~ f) = {(f /. (len f))} holds
(
L~ h is_S-P_arc_joining f /. 1,
p &
L~ h c= (L~ f) \/ (Ball (u,r)) )
Lm1:
TopSpaceMetr (Euclid 2) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #)
by EUCLID:def 8;