:: by Yatsuka Nakamura and Jaros{\l}aw Kotowicz

::

:: Received August 24, 1992

:: Copyright (c) 1992-2012 Association of Mizar Users

begin

definition

let P be Subset of (TOP-REAL 2);

let p, q be Point of (TOP-REAL 2);

end;
let p, q be Point of (TOP-REAL 2);

pred P is_S-P_arc_joining p,q means :Def1: :: TOPREAL4:def 1

ex f being FinSequence of (TOP-REAL 2) st

( f is being_S-Seq & P = L~ f & p = f /. 1 & q = f /. (len f) );

ex f being FinSequence of (TOP-REAL 2) st

( f is being_S-Seq & P = L~ f & p = f /. 1 & q = f /. (len f) );

:: deftheorem Def1 defines is_S-P_arc_joining TOPREAL4:def 1 :

for P being Subset of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) holds

( P is_S-P_arc_joining p,q iff ex f being FinSequence of (TOP-REAL 2) st

( f is being_S-Seq & P = L~ f & p = f /. 1 & q = f /. (len f) ) );

for P being Subset of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) holds

( P is_S-P_arc_joining p,q iff ex f being FinSequence of (TOP-REAL 2) st

( f is being_S-Seq & P = L~ f & p = f /. 1 & q = f /. (len f) ) );

definition

let P be Subset of (TOP-REAL 2);

end;
attr P is being_special_polygon means :: TOPREAL4:def 2

ex p1, p2 being Point of (TOP-REAL 2) ex P1, P2 being Subset of (TOP-REAL 2) st

( p1 <> p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 );

ex p1, p2 being Point of (TOP-REAL 2) ex P1, P2 being Subset of (TOP-REAL 2) st

( p1 <> p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 );

:: deftheorem defines being_special_polygon TOPREAL4:def 2 :

for P being Subset of (TOP-REAL 2) holds

( P is being_special_polygon iff ex p1, p2 being Point of (TOP-REAL 2) ex P1, P2 being Subset of (TOP-REAL 2) st

( p1 <> p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) );

for P being Subset of (TOP-REAL 2) holds

( P is being_special_polygon iff ex p1, p2 being Point of (TOP-REAL 2) ex P1, P2 being Subset of (TOP-REAL 2) st

( p1 <> p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) );

:: deftheorem Def3 defines being_Region TOPREAL4:def 3 :

for T being TopStruct

for P being Subset of T holds

( P is being_Region iff ( P is open & P is connected ) );

for T being TopStruct

for P being Subset of T holds

( P is being_Region iff ( P is open & P is connected ) );

theorem Th1: :: TOPREAL4:1

for P being Subset of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st P is_S-P_arc_joining p,q holds

P is being_S-P_arc

for p, q being Point of (TOP-REAL 2) st P is_S-P_arc_joining p,q holds

P is being_S-P_arc

proof end;

theorem Th2: :: TOPREAL4:2

for P being Subset of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st P is_S-P_arc_joining p,q holds

P is_an_arc_of p,q

for p, q being Point of (TOP-REAL 2) st P is_S-P_arc_joining p,q holds

P is_an_arc_of p,q

proof end;

theorem Th3: :: TOPREAL4:3

for P being Subset of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st P is_S-P_arc_joining p,q holds

( p in P & q in P )

for p, q being Point of (TOP-REAL 2) st P is_S-P_arc_joining p,q holds

( p in P & q in P )

proof end;

theorem :: TOPREAL4:4

for P being Subset of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st P is_S-P_arc_joining p,q holds

p <> q

for p, q being Point of (TOP-REAL 2) st P is_S-P_arc_joining p,q holds

p <> q

proof end;

theorem :: TOPREAL4:5

for P being Subset of (TOP-REAL 2) st P is being_special_polygon holds

P is being_simple_closed_curve

P is being_simple_closed_curve

proof end;

theorem Th6: :: TOPREAL4:6

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) & f = <*p,|[(p `1),(((p `2) + (q `2)) / 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) )

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) & f = <*p,|[(p `1),(((p `2) + (q `2)) / 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) )

proof end;

theorem Th7: :: TOPREAL4:7

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) & f = <*p,|[(((p `1) + (q `1)) / 2),(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) )

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) & f = <*p,|[(((p `1) + (q `1)) / 2),(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) )

proof end;

theorem Th8: :: TOPREAL4:8

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) )

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) )

proof end;

theorem Th9: :: TOPREAL4:9

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) )

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) )

proof end;

theorem Th10: :: TOPREAL4:10

for p, q being Point of (TOP-REAL 2)

for r being Real

for u being Point of (Euclid 2) st p <> q & p in Ball (u,r) & q in Ball (u,r) holds

ex P being Subset of (TOP-REAL 2) st

( P is_S-P_arc_joining p,q & P c= Ball (u,r) )

for r being Real

for u being Point of (Euclid 2) st p <> q & p in Ball (u,r) & q in Ball (u,r) holds

ex P being Subset of (TOP-REAL 2) st

( P is_S-P_arc_joining p,q & P c= Ball (u,r) )

proof end;

theorem Th11: :: TOPREAL4:11

for p being Point of (TOP-REAL 2)

for f, h being FinSequence of (TOP-REAL 2) st p <> f /. 1 & (f /. 1) `2 = p `2 & f is being_S-Seq & p in LSeg (f,1) & h = <*(f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p*> holds

( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) )

for f, h being FinSequence of (TOP-REAL 2) st p <> f /. 1 & (f /. 1) `2 = p `2 & f is being_S-Seq & p in LSeg (f,1) & h = <*(f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p*> holds

( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) )

proof end;

theorem Th12: :: TOPREAL4:12

for p being Point of (TOP-REAL 2)

for f, h being FinSequence of (TOP-REAL 2) st p <> f /. 1 & (f /. 1) `1 = p `1 & f is being_S-Seq & p in LSeg (f,1) & h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|,p*> holds

( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) )

for f, h being FinSequence of (TOP-REAL 2) st p <> f /. 1 & (f /. 1) `1 = p `1 & f is being_S-Seq & p in LSeg (f,1) & h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|,p*> holds

( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) )

proof end;

theorem Th13: :: TOPREAL4:13

for p being Point of (TOP-REAL 2)

for f, h being FinSequence of (TOP-REAL 2)

for i being Element of NAT st f is being_S-Seq & i in dom f & i + 1 in dom f & i > 1 & p in LSeg (f,i) & p <> f /. i & h = (f | i) ^ <*p*> holds

( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),p)) )

for f, h being FinSequence of (TOP-REAL 2)

for i being Element of NAT st f is being_S-Seq & i in dom f & i + 1 in dom f & i > 1 & p in LSeg (f,i) & p <> f /. i & h = (f | i) ^ <*p*> holds

( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),p)) )

proof end;

theorem Th14: :: TOPREAL4:14

for f, h being FinSequence of (TOP-REAL 2) st f /. 2 <> f /. 1 & f is being_S-Seq & (f /. 2) `2 = (f /. 1) `2 & h = <*(f /. 1),|[((((f /. 1) `1) + ((f /. 2) `1)) / 2),((f /. 1) `2)]|,(f /. 2)*> holds

( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. 2 & L~ h is_S-P_arc_joining f /. 1,f /. 2 & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),(f /. 2))) & L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) )

( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. 2 & L~ h is_S-P_arc_joining f /. 1,f /. 2 & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),(f /. 2))) & L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) )

proof end;

theorem Th15: :: TOPREAL4:15

for f, h being FinSequence of (TOP-REAL 2) st f /. 2 <> f /. 1 & f is being_S-Seq & (f /. 2) `1 = (f /. 1) `1 & h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + ((f /. 2) `2)) / 2)]|,(f /. 2)*> holds

( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. 2 & L~ h is_S-P_arc_joining f /. 1,f /. 2 & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),(f /. 2))) & L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) )

( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. 2 & L~ h is_S-P_arc_joining f /. 1,f /. 2 & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),(f /. 2))) & L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) )

proof end;

theorem Th16: :: TOPREAL4:16

for f, h being FinSequence of (TOP-REAL 2)

for i being Element of NAT st f is being_S-Seq & i > 2 & i in dom f & h = f | i holds

( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. i & L~ h is_S-P_arc_joining f /. 1,f /. i & L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. i))) )

for i being Element of NAT st f is being_S-Seq & i > 2 & i in dom f & h = f | i holds

( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. i & L~ h is_S-P_arc_joining f /. 1,f /. i & L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. i))) )

proof end;

theorem Th17: :: TOPREAL4:17

for p being Point of (TOP-REAL 2)

for f being FinSequence of (TOP-REAL 2)

for n being Element of NAT st p <> f /. 1 & f is being_S-Seq & p in LSeg (f,n) holds

ex h being FinSequence of (TOP-REAL 2) st

( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

for f being FinSequence of (TOP-REAL 2)

for n being Element of NAT st p <> f /. 1 & f is being_S-Seq & p in LSeg (f,n) holds

ex h being FinSequence of (TOP-REAL 2) st

( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) )

proof end;

theorem Th18: :: TOPREAL4:18

for p being Point of (TOP-REAL 2)

for f being FinSequence of (TOP-REAL 2) st p <> f /. 1 & f is being_S-Seq & p in L~ f holds

ex h being FinSequence of (TOP-REAL 2) st

( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f )

for f being FinSequence of (TOP-REAL 2) st p <> f /. 1 & f is being_S-Seq & p in L~ f holds

ex h being FinSequence of (TOP-REAL 2) st

( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f )

proof end;

theorem Th19: :: TOPREAL4:19

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 ( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) ) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} & h = f ^ <*p*> holds

( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

for f, h being FinSequence of (TOP-REAL 2)

for r being Real

for u being Point of (Euclid 2) st ( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) ) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} & h = f ^ <*p*> holds

( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

proof end;

theorem Th20: :: TOPREAL4:20

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)) )

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)) )

proof end;

theorem Th21: :: TOPREAL4:21

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)) )

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)) )

proof end;

theorem Th22: :: TOPREAL4:22

for p 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 not f /. 1 in Ball (u,r) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & not p in L~ f holds

ex h being FinSequence of (TOP-REAL 2) st

( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

for f being FinSequence of (TOP-REAL 2)

for r being Real

for u being Point of (Euclid 2) st not f /. 1 in Ball (u,r) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & not p in L~ f holds

ex h being FinSequence of (TOP-REAL 2) st

( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

proof end;

theorem Th23: :: TOPREAL4:23

for R being Subset of (TOP-REAL 2)

for p, p1, p2 being Point of (TOP-REAL 2)

for P being Subset of (TOP-REAL 2)

for r being Real

for u being Point of (Euclid 2) st p <> p1 & P is_S-P_arc_joining p1,p2 & P c= R & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= R holds

ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )

for p, p1, p2 being Point of (TOP-REAL 2)

for P being Subset of (TOP-REAL 2)

for r being Real

for u being Point of (Euclid 2) st p <> p1 & P is_S-P_arc_joining p1,p2 & P c= R & p in Ball (u,r) & p2 in Ball (u,r) & Ball (u,r) c= R holds

ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p & P1 c= R )

proof end;

Lm1: TopSpaceMetr (Euclid 2) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #)

by EUCLID:def 8;

theorem Th24: :: TOPREAL4:24

for R, P being Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st R is being_Region & P = { q where q is Point of (TOP-REAL 2) : ( q <> p & q in R & ( for P1 being Subset of (TOP-REAL 2) holds

( not P1 is_S-P_arc_joining p,q or not P1 c= R ) ) ) } holds

P is open

for p being Point of (TOP-REAL 2) st R is being_Region & P = { q where q is Point of (TOP-REAL 2) : ( q <> p & q in R & ( for P1 being Subset of (TOP-REAL 2) holds

( not P1 is_S-P_arc_joining p,q or not P1 c= R ) ) ) } holds

P is open

proof end;

theorem Th25: :: TOPREAL4:25

for p being Point of (TOP-REAL 2)

for R, P being Subset of (TOP-REAL 2) st R is being_Region & p in R & P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q & P1 c= R ) ) } holds

P is open

for R, P being Subset of (TOP-REAL 2) st R is being_Region & p in R & P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q & P1 c= R ) ) } holds

P is open

proof end;

theorem Th26: :: TOPREAL4:26

for p being Point of (TOP-REAL 2)

for R, P being Subset of (TOP-REAL 2) st p in R & P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q & P1 c= R ) ) } holds

P c= R

for R, P being Subset of (TOP-REAL 2) st p in R & P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q & P1 c= R ) ) } holds

P c= R

proof end;

theorem Th27: :: TOPREAL4:27

for p being Point of (TOP-REAL 2)

for R, P being Subset of (TOP-REAL 2) st R is being_Region & p in R & P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q & P1 c= R ) ) } holds

R c= P

for R, P being Subset of (TOP-REAL 2) st R is being_Region & p in R & P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q & P1 c= R ) ) } holds

R c= P

proof end;

theorem :: TOPREAL4:28

for p being Point of (TOP-REAL 2)

for R, P being Subset of (TOP-REAL 2) st R is being_Region & p in R & P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q & P1 c= R ) ) } holds

R = P

for R, P being Subset of (TOP-REAL 2) st R is being_Region & p in R & P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q & P1 c= R ) ) } holds

R = P

proof end;

theorem :: TOPREAL4:29

for p, q being Point of (TOP-REAL 2)

for R being Subset of (TOP-REAL 2) st R is being_Region & p in R & q in R & p <> q holds

ex P being Subset of (TOP-REAL 2) st

( P is_S-P_arc_joining p,q & P c= R )

for R being Subset of (TOP-REAL 2) st R is being_Region & p in R & q in R & p <> q holds

ex P being Subset of (TOP-REAL 2) st

( P is_S-P_arc_joining p,q & P c= R )

proof end;