:: TOPREAL4 semantic presentation begin definition let P be Subset of (TOP-REAL 2); let p, q be Point of (TOP-REAL 2); predP 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) ); end; :: 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) ) ); definition let P be Subset of (TOP-REAL 2); attrP 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 ); end; :: 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 ) ); definition let T be TopStruct ; let P be Subset of T; attrP is being_Region means :Def3: :: TOPREAL4:def 3 ( P is open & P is connected ); end; :: 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 ) ); 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 proof let P be Subset of (TOP-REAL 2); ::_thesis: 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 let p, q be Point of (TOP-REAL 2); ::_thesis: ( P is_S-P_arc_joining p,q implies P is being_S-P_arc ) assume P is_S-P_arc_joining p,q ; ::_thesis: P is being_S-P_arc then ex f being FinSequence of (TOP-REAL 2) st ( f is being_S-Seq & P = L~ f & p = f /. 1 & q = f /. (len f) ) by Def1; hence P is being_S-P_arc by TOPREAL1:def_9; ::_thesis: verum 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 proof let P be Subset of (TOP-REAL 2); ::_thesis: 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 let p, q be Point of (TOP-REAL 2); ::_thesis: ( P is_S-P_arc_joining p,q implies P is_an_arc_of p,q ) assume P is_S-P_arc_joining p,q ; ::_thesis: P is_an_arc_of p,q then ex h being FinSequence of (TOP-REAL 2) st ( h is being_S-Seq & P = L~ h & p = h /. 1 & q = h /. (len h) ) by Def1; hence P is_an_arc_of p,q by TOPREAL1:25; ::_thesis: verum 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 ) proof let P be Subset of (TOP-REAL 2); ::_thesis: 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 ) let p, q be Point of (TOP-REAL 2); ::_thesis: ( P is_S-P_arc_joining p,q implies ( p in P & q in P ) ) assume P is_S-P_arc_joining p,q ; ::_thesis: ( p in P & q in P ) then P is_an_arc_of p,q by Th2; hence ( p in P & q in P ) by TOPREAL1:1; ::_thesis: verum 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 proof let P be Subset of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st P is_S-P_arc_joining p,q holds p <> q let p, q be Point of (TOP-REAL 2); ::_thesis: ( P is_S-P_arc_joining p,q implies p <> q ) assume that A1: P is_S-P_arc_joining p,q and A2: p = q ; ::_thesis: contradiction consider f being FinSequence of (TOP-REAL 2) such that A3: f is being_S-Seq and P = L~ f and A4: ( p = f /. 1 & q = f /. (len f) ) by A1, Def1; len f >= 2 by A3, TOPREAL1:def_8; then ( Seg (len f) = dom f & len f >= 1 ) by FINSEQ_1:def_3, XXREAL_0:2; then A5: ( len f in dom f & 1 in dom f ) by FINSEQ_1:1; ( f is one-to-one & 1 <> len f ) by A3, TOPREAL1:def_8; hence contradiction by A2, A4, A5, PARTFUN2:10; ::_thesis: verum 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 proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P is being_special_polygon implies P is being_simple_closed_curve ) given p1, p2 being Point of (TOP-REAL 2), P1, P2 being Subset of (TOP-REAL 2) such that A1: ( p1 <> p2 & p1 in P & p2 in P ) and A2: ( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 ) and A3: P1 /\ P2 = {p1,p2} and A4: P = P1 \/ P2 ; :: according to TOPREAL4:def_2 ::_thesis: P is being_simple_closed_curve reconsider P1 = P1, P2 = P2 as non empty Subset of (TOP-REAL 2) by A3; ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 ) by A2, Th2; hence P is being_simple_closed_curve by A1, A3, A4, TOPREAL2:6; ::_thesis: verum 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) ) proof let p, q be Point of (TOP-REAL 2); ::_thesis: 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) ) let f be FinSequence of (TOP-REAL 2); ::_thesis: 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) ) let r be Real; ::_thesis: 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) ) let u be Point of (Euclid 2); ::_thesis: ( 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*> implies ( 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) ) ) assume that A1: p `1 = q `1 and A2: p `2 <> q `2 and A3: ( p in Ball (u,r) & q in Ball (u,r) ) and A4: f = <*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> ; ::_thesis: ( 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) ) thus A5: ( f is being_S-Seq & f /. 1 = p & f /. (len f) = q ) by A1, A2, A4, TOPREAL3:36; ::_thesis: ( L~ f is_S-P_arc_joining p,q & L~ f c= Ball (u,r) ) ( p = |[(p `1),(p `2)]| & q = |[(q `1),(q `2)]| ) by EUCLID:53; then |[(p `1),(((p `2) + (q `2)) / 2)]| in Ball (u,r) by A1, A3, TOPREAL3:23; then A6: ( LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|) c= Ball (u,r) & LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q) c= Ball (u,r) ) by A3, TOPREAL3:21; thus L~ f is_S-P_arc_joining p,q by A5, Def1; ::_thesis: L~ f c= Ball (u,r) L~ f = (LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|)) \/ (LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q)) by A4, TOPREAL3:16; hence L~ f c= Ball (u,r) by A6, XBOOLE_1:8; ::_thesis: verum 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) ) proof let p, q be Point of (TOP-REAL 2); ::_thesis: 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) ) let f be FinSequence of (TOP-REAL 2); ::_thesis: 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) ) let r be Real; ::_thesis: 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) ) let u be Point of (Euclid 2); ::_thesis: ( 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*> implies ( 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) ) ) assume that A1: p `1 <> q `1 and A2: p `2 = q `2 and A3: ( p in Ball (u,r) & q in Ball (u,r) ) and A4: f = <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> ; ::_thesis: ( 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) ) thus A5: ( f is being_S-Seq & f /. 1 = p & f /. (len f) = q ) by A1, A2, A4, TOPREAL3:37; ::_thesis: ( L~ f is_S-P_arc_joining p,q & L~ f c= Ball (u,r) ) ( p = |[(p `1),(p `2)]| & q = |[(q `1),(q `2)]| ) by EUCLID:53; then |[(((p `1) + (q `1)) / 2),(p `2)]| in Ball (u,r) by A2, A3, TOPREAL3:24; then A6: ( LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|) c= Ball (u,r) & LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q) c= Ball (u,r) ) by A3, TOPREAL3:21; thus L~ f is_S-P_arc_joining p,q by A5, Def1; ::_thesis: L~ f c= Ball (u,r) L~ f = (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) \/ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) by A4, TOPREAL3:16; hence L~ f c= Ball (u,r) by A6, XBOOLE_1:8; ::_thesis: verum 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) ) proof let p, q be Point of (TOP-REAL 2); ::_thesis: 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) ) let f be FinSequence of (TOP-REAL 2); ::_thesis: 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) ) let r be Real; ::_thesis: 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) ) let u be Point of (Euclid 2); ::_thesis: ( 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*> implies ( 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) ) ) assume that A1: ( p `1 <> q `1 & p `2 <> q `2 ) and A2: p in Ball (u,r) and A3: q in Ball (u,r) and A4: |[(p `1),(q `2)]| in Ball (u,r) and A5: f = <*p,|[(p `1),(q `2)]|,q*> ; ::_thesis: ( 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) ) thus A6: ( f is being_S-Seq & f /. 1 = p & f /. (len f) = q ) by A1, A5, TOPREAL3:34; ::_thesis: ( L~ f is_S-P_arc_joining p,q & L~ f c= Ball (u,r) ) A7: LSeg (|[(p `1),(q `2)]|,q) c= Ball (u,r) by A3, A4, TOPREAL3:21; thus L~ f is_S-P_arc_joining p,q by A6, Def1; ::_thesis: L~ f c= Ball (u,r) ( L~ f = (LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q)) & LSeg (p,|[(p `1),(q `2)]|) c= Ball (u,r) ) by A2, A4, A5, TOPREAL3:16, TOPREAL3:21; hence L~ f c= Ball (u,r) by A7, XBOOLE_1:8; ::_thesis: verum 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) ) proof let p, q be Point of (TOP-REAL 2); ::_thesis: 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) ) let f be FinSequence of (TOP-REAL 2); ::_thesis: 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) ) let r be Real; ::_thesis: 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) ) let u be Point of (Euclid 2); ::_thesis: ( 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*> implies ( 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) ) ) assume that A1: ( p `1 <> q `1 & p `2 <> q `2 ) and A2: p in Ball (u,r) and A3: q in Ball (u,r) and A4: |[(q `1),(p `2)]| in Ball (u,r) and A5: f = <*p,|[(q `1),(p `2)]|,q*> ; ::_thesis: ( 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) ) thus A6: ( f is being_S-Seq & f /. 1 = p & f /. (len f) = q ) by A1, A5, TOPREAL3:35; ::_thesis: ( L~ f is_S-P_arc_joining p,q & L~ f c= Ball (u,r) ) A7: LSeg (|[(q `1),(p `2)]|,q) c= Ball (u,r) by A3, A4, TOPREAL3:21; thus L~ f is_S-P_arc_joining p,q by A6, Def1; ::_thesis: L~ f c= Ball (u,r) ( L~ f = (LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q)) & LSeg (p,|[(q `1),(p `2)]|) c= Ball (u,r) ) by A2, A4, A5, TOPREAL3:16, TOPREAL3:21; hence L~ f c= Ball (u,r) by A7, XBOOLE_1:8; ::_thesis: verum 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) ) proof let p, q be Point of (TOP-REAL 2); ::_thesis: 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) ) let r be Real; ::_thesis: 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) ) let u be Point of (Euclid 2); ::_thesis: ( p <> q & p in Ball (u,r) & q in Ball (u,r) implies ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) ) assume that A1: p <> q and A2: ( p in Ball (u,r) & q in Ball (u,r) ) ; ::_thesis: ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) now__::_thesis:_ex_P_being_Subset_of_(TOP-REAL_2)_st_ (_P_is_S-P_arc_joining_p,q_&_P_c=_Ball_(u,r)_) percases ( p `1 <> q `1 or p `2 <> q `2 ) by A1, TOPREAL3:6; supposeA3: p `1 <> q `1 ; ::_thesis: ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) now__::_thesis:_ex_P_being_Subset_of_(TOP-REAL_2)_st_ (_P_is_S-P_arc_joining_p,q_&_P_c=_Ball_(u,r)_) percases ( p `2 = q `2 or p `2 <> q `2 ) ; supposeA4: p `2 = q `2 ; ::_thesis: ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) reconsider P = L~ <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> as Subset of (TOP-REAL 2) ; take P = P; ::_thesis: ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) thus ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) by A2, A3, A4, Th7; ::_thesis: verum end; supposeA5: p `2 <> q `2 ; ::_thesis: ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) A6: ( p = |[(p `1),(p `2)]| & q = |[(q `1),(q `2)]| ) by EUCLID:53; now__::_thesis:_ex_P_being_Subset_of_(TOP-REAL_2)_st_ (_P_is_S-P_arc_joining_p,q_&_P_c=_Ball_(u,r)_) percases ( |[(p `1),(q `2)]| in Ball (u,r) or |[(q `1),(p `2)]| in Ball (u,r) ) by A2, A6, TOPREAL3:25; supposeA7: |[(p `1),(q `2)]| in Ball (u,r) ; ::_thesis: ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) reconsider P = L~ <*p,|[(p `1),(q `2)]|,q*> as Subset of (TOP-REAL 2) ; take P = P; ::_thesis: ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) thus ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) by A2, A3, A5, A7, Th8; ::_thesis: verum end; supposeA8: |[(q `1),(p `2)]| in Ball (u,r) ; ::_thesis: ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) reconsider P = L~ <*p,|[(q `1),(p `2)]|,q*> as Subset of (TOP-REAL 2) ; take P = P; ::_thesis: ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) thus ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) by A2, A3, A5, A8, Th9; ::_thesis: verum end; end; end; hence ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) ; ::_thesis: verum end; end; end; hence ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) ; ::_thesis: verum end; supposeA9: p `2 <> q `2 ; ::_thesis: ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) now__::_thesis:_ex_P_being_Subset_of_(TOP-REAL_2)_st_ (_P_is_S-P_arc_joining_p,q_&_P_c=_Ball_(u,r)_) percases ( p `1 = q `1 or p `1 <> q `1 ) ; supposeA10: p `1 = q `1 ; ::_thesis: ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) reconsider P = L~ <*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> as Subset of (TOP-REAL 2) ; take P = P; ::_thesis: ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) thus ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) by A2, A9, A10, Th6; ::_thesis: verum end; supposeA11: p `1 <> q `1 ; ::_thesis: ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) A12: ( p = |[(p `1),(p `2)]| & q = |[(q `1),(q `2)]| ) by EUCLID:53; now__::_thesis:_ex_P_being_Subset_of_(TOP-REAL_2)_st_ (_P_is_S-P_arc_joining_p,q_&_P_c=_Ball_(u,r)_) percases ( |[(p `1),(q `2)]| in Ball (u,r) or |[(q `1),(p `2)]| in Ball (u,r) ) by A2, A12, TOPREAL3:25; supposeA13: |[(p `1),(q `2)]| in Ball (u,r) ; ::_thesis: ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) reconsider P = L~ <*p,|[(p `1),(q `2)]|,q*> as Subset of (TOP-REAL 2) ; take P = P; ::_thesis: ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) thus ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) by A2, A9, A11, A13, Th8; ::_thesis: verum end; supposeA14: |[(q `1),(p `2)]| in Ball (u,r) ; ::_thesis: ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) reconsider P = L~ <*p,|[(q `1),(p `2)]|,q*> as Subset of (TOP-REAL 2) ; take P = P; ::_thesis: ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) thus ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) by A2, A9, A11, A14, Th9; ::_thesis: verum end; end; end; hence ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) ; ::_thesis: verum end; end; end; hence ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) ; ::_thesis: verum end; end; end; hence ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) ; ::_thesis: verum 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)) ) proof let p be Point of (TOP-REAL 2); ::_thesis: 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)) ) let f, h be FinSequence of (TOP-REAL 2); ::_thesis: ( 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*> implies ( 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)) ) ) assume that A1: p <> f /. 1 and A2: (f /. 1) `2 = p `2 and A3: f is being_S-Seq and A4: p in LSeg (f,1) and A5: h = <*(f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p*> ; ::_thesis: ( 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)) ) set p1 = f /. 1; set q = f /. (1 + 1); A6: L~ h = (LSeg ((f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|)) \/ (LSeg (|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p)) by A5, TOPREAL3:16; A7: len f >= 2 by A3, TOPREAL1:def_8; then A8: LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by TOPREAL1:def_3; A9: (f /. 1) `1 <> p `1 by A1, A2, TOPREAL3:6; hence A10: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p ) by A2, A5, TOPREAL3:37; ::_thesis: ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) ) f /. 1 in LSeg ((f /. 1),(f /. (1 + 1))) by RLTOPSP1:68; then A11: LSeg ((f /. 1),p) c= LSeg ((f /. 1),(f /. (1 + 1))) by A4, A8, TOPREAL1:6; A12: Seg (len f) = dom f by FINSEQ_1:def_3; thus L~ h is_S-P_arc_joining f /. 1,p by A10, Def1; ::_thesis: ( L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) ) A13: LSeg (f,1) c= L~ f by TOPREAL3:19; (LSeg ((f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|)) \/ (LSeg (|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p)) = LSeg ((f /. 1),p) by A2, A9, TOPREAL1:5, TOPREAL3:13; hence L~ h c= L~ f by A8, A11, A6, A13, XBOOLE_1:1; ::_thesis: L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) len f >= 1 by A7, XXREAL_0:2; then Seg 1 c= Seg (len f) by FINSEQ_1:5; then ( f | 1 = f | (Seg 1) & (dom f) /\ (Seg 1) = Seg 1 ) by A12, FINSEQ_1:def_15, XBOOLE_1:28; then dom (f | 1) = Seg 1 by RELAT_1:61; then len (f | 1) = 1 by FINSEQ_1:def_3; then L~ (f | 1) = {} by TOPREAL1:22; hence L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) by A2, A9, A6, TOPREAL1:5, TOPREAL3:13; ::_thesis: verum 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)) ) proof let p be Point of (TOP-REAL 2); ::_thesis: 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)) ) let f, h be FinSequence of (TOP-REAL 2); ::_thesis: ( 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*> implies ( 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)) ) ) set p1 = f /. 1; assume that A1: p <> f /. 1 and A2: (f /. 1) `1 = p `1 and A3: f is being_S-Seq and A4: p in LSeg (f,1) and A5: h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|,p*> ; ::_thesis: ( 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)) ) A6: L~ h = (LSeg ((f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|)) \/ (LSeg (|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|,p)) by A5, TOPREAL3:16; set q = f /. (1 + 1); A7: len f >= 2 by A3, TOPREAL1:def_8; then A8: LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by TOPREAL1:def_3; A9: (f /. 1) `2 <> p `2 by A1, A2, TOPREAL3:6; hence A10: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p ) by A2, A5, TOPREAL3:36; ::_thesis: ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) ) f /. 1 in LSeg ((f /. 1),(f /. (1 + 1))) by RLTOPSP1:68; then A11: LSeg ((f /. 1),p) c= LSeg ((f /. 1),(f /. (1 + 1))) by A4, A8, TOPREAL1:6; A12: Seg (len f) = dom f by FINSEQ_1:def_3; thus L~ h is_S-P_arc_joining f /. 1,p by A10, Def1; ::_thesis: ( L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) ) A13: LSeg (f,1) c= L~ f by TOPREAL3:19; (LSeg ((f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|)) \/ (LSeg (|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|,p)) = LSeg ((f /. 1),p) by A2, A9, TOPREAL1:5, TOPREAL3:14; hence L~ h c= L~ f by A8, A11, A6, A13, XBOOLE_1:1; ::_thesis: L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) len f >= 1 by A7, XXREAL_0:2; then Seg 1 c= Seg (len f) by FINSEQ_1:5; then ( f | 1 = f | (Seg 1) & (dom f) /\ (Seg 1) = Seg 1 ) by A12, FINSEQ_1:def_15, XBOOLE_1:28; then dom (f | 1) = Seg 1 by RELAT_1:61; then len (f | 1) = 1 by FINSEQ_1:def_3; then L~ (f | 1) = {} by TOPREAL1:22; hence L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) by A2, A9, A6, TOPREAL1:5, TOPREAL3:14; ::_thesis: verum 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)) ) proof let p be Point of (TOP-REAL 2); ::_thesis: 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)) ) let f, h be FinSequence of (TOP-REAL 2); ::_thesis: 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)) ) let i be Element of NAT ; ::_thesis: ( 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*> implies ( 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)) ) ) set p1 = f /. 1; set q = f /. i; assume that A1: f is being_S-Seq and A2: i in dom f and A3: i + 1 in dom f and A4: i > 1 and A5: p in LSeg (f,i) and A6: p <> f /. i and A7: h = (f | i) ^ <*p*> ; ::_thesis: ( 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)) ) A8: f is one-to-one by A1, TOPREAL1:def_8; set v = f | i; A9: f | i = f | (Seg i) by FINSEQ_1:def_15; then A10: dom (f | i) = (dom f) /\ (Seg i) by RELAT_1:61; A11: Seg (len h) = dom h by FINSEQ_1:def_3; A12: f is unfolded by A1, TOPREAL1:def_8; A13: f is special by A1, TOPREAL1:def_8; A14: f is s.n.c. by A1, TOPREAL1:def_8; set q1 = f /. i; set q2 = f /. (i + 1); A15: Seg (len f) = dom f by FINSEQ_1:def_3; then A16: i + 1 <= len f by A3, FINSEQ_1:1; then A17: p in LSeg ((f /. i),(f /. (i + 1))) by A4, A5, TOPREAL1:def_3; A18: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A4, A16, TOPREAL1:def_3; A19: LSeg (f,i) = LSeg ((f /. (i + 1)),(f /. i)) by A4, A16, TOPREAL1:def_3; i <> i + 1 ; then A20: f /. i <> f /. (i + 1) by A2, A3, A8, PARTFUN2:10; A21: f /. i in LSeg ((f /. i),(f /. (i + 1))) by RLTOPSP1:68; A22: ( f /. i = |[((f /. i) `1),((f /. i) `2)]| & f /. (i + 1) = |[((f /. (i + 1)) `1),((f /. (i + 1)) `2)]| ) by EUCLID:53; A23: i <= len f by A2, A15, FINSEQ_1:1; then Seg i c= dom f by A15, FINSEQ_1:5; then A24: dom (f | i) = Seg i by A10, XBOOLE_1:28; then A25: len (f | i) = i by FINSEQ_1:def_3; then A26: len h = i + (len <*p*>) by A7, FINSEQ_1:22 .= i + 1 by FINSEQ_1:39 ; then A27: h /. (len h) = p by A7, A25, FINSEQ_4:67; A28: i in dom (f | i) by A4, A24, FINSEQ_1:1; then A29: h /. i = (f | i) /. i by A7, FINSEQ_4:68 .= f /. i by A28, FINSEQ_4:70 ; then A30: LSeg (h,i) = LSeg ((f /. i),p) by A4, A26, A27, TOPREAL1:def_3; A31: 1 + 1 <= i by A4, NAT_1:13; thus A32: h is being_S-Seq ::_thesis: ( 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 now__::_thesis:_for_x,_y_being_set_holds_ (_not_x_in_dom_h_or_not_y_in_dom_h_or_not_h_._x_=_h_._y_or_not_x_<>_y_) set Z = { m where m is Element of NAT : ( 1 <= m & m <= len h ) } ; given x, y being set such that A33: x in dom h and A34: y in dom h and A35: h . x = h . y and A36: x <> y ; ::_thesis: contradiction x in { m where m is Element of NAT : ( 1 <= m & m <= len h ) } by A11, A33, FINSEQ_1:def_1; then consider k1 being Element of NAT such that A37: k1 = x and A38: 1 <= k1 and A39: k1 <= len h ; y in { m where m is Element of NAT : ( 1 <= m & m <= len h ) } by A11, A34, FINSEQ_1:def_1; then consider k2 being Element of NAT such that A40: k2 = y and A41: 1 <= k2 and A42: k2 <= len h ; A43: h /. k1 = h . y by A33, A35, A37, PARTFUN1:def_6 .= h /. k2 by A34, A40, PARTFUN1:def_6 ; k2 <= len f by A26, A16, A42, XXREAL_0:2; then A44: k2 in dom f by A15, A41, FINSEQ_1:1; k1 <= len f by A26, A16, A39, XXREAL_0:2; then A45: k1 in dom f by A15, A38, FINSEQ_1:1; A46: k1 + (1 + 1) = (k1 + 1) + 1 ; A47: k2 + (1 + 1) = (k2 + 1) + 1 ; now__::_thesis:_contradiction percases ( ( k1 = i + 1 & k2 = i + 1 ) or ( k1 = i + 1 & k2 < i + 1 ) or ( k1 < i + 1 & k2 = i + 1 ) or ( k1 < i + 1 & k2 < i + 1 ) ) by A26, A39, A42, XXREAL_0:1; suppose ( k1 = i + 1 & k2 = i + 1 ) ; ::_thesis: contradiction hence contradiction by A36, A37, A40; ::_thesis: verum end; supposeA48: ( k1 = i + 1 & k2 < i + 1 ) ; ::_thesis: contradiction then A49: k2 + 1 <= k1 by NAT_1:13; now__::_thesis:_contradiction percases ( k2 + 1 = k1 or k2 + 1 < k1 ) by A49, XXREAL_0:1; suppose k2 + 1 = k1 ; ::_thesis: contradiction hence contradiction by A6, A7, A25, A29, A43, A48, FINSEQ_4:67; ::_thesis: verum end; suppose k2 + 1 < k1 ; ::_thesis: contradiction then A50: k2 + 1 <= i by A48, NAT_1:13; now__::_thesis:_contradiction percases ( k2 + 1 = i or k2 + 1 < i ) by A50, XXREAL_0:1; supposeA51: k2 + 1 = i ; ::_thesis: contradiction then k2 <= i by NAT_1:11; then A52: k2 in dom (f | i) by A24, A41, FINSEQ_1:1; then A53: h /. k2 = (f | i) /. k2 by A7, FINSEQ_4:68 .= f /. k2 by A52, FINSEQ_4:70 ; k2 + 1 <= len f by A2, A15, A51, FINSEQ_1:1; then A54: f /. k2 in LSeg (f,k2) by A41, TOPREAL1:21; (LSeg (f,k2)) /\ (LSeg (f,i)) = {(f /. i)} by A12, A16, A41, A47, A51, TOPREAL1:def_6; then f /. k2 in {(f /. i)} by A5, A26, A27, A43, A48, A54, A53, XBOOLE_0:def_4; then A55: f /. k2 = f /. i by TARSKI:def_1; k2 < i by A51, NAT_1:13; hence contradiction by A2, A8, A44, A55, PARTFUN2:10; ::_thesis: verum end; supposeA56: k2 + 1 < i ; ::_thesis: contradiction then A57: k2 + 1 <= len f by A23, XXREAL_0:2; A58: LSeg (f,k2) misses LSeg (f,i) by A14, A56, TOPREAL1:def_7; k2 <= k2 + 1 by NAT_1:11; then k2 <= i by A56, XXREAL_0:2; then A59: k2 in dom (f | i) by A24, A41, FINSEQ_1:1; then h /. k2 = (f | i) /. k2 by A7, FINSEQ_4:68 .= f /. k2 by A59, FINSEQ_4:70 ; then p in LSeg (f,k2) by A26, A27, A41, A43, A48, A57, TOPREAL1:21; hence contradiction by A5, A58, XBOOLE_0:3; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; supposeA60: ( k1 < i + 1 & k2 = i + 1 ) ; ::_thesis: contradiction then A61: k1 + 1 <= k2 by NAT_1:13; now__::_thesis:_contradiction percases ( k1 + 1 = k2 or k1 + 1 < k2 ) by A61, XXREAL_0:1; suppose k1 + 1 = k2 ; ::_thesis: contradiction hence contradiction by A6, A7, A25, A29, A43, A60, FINSEQ_4:67; ::_thesis: verum end; suppose k1 + 1 < k2 ; ::_thesis: contradiction then A62: k1 + 1 <= i by A60, NAT_1:13; now__::_thesis:_contradiction percases ( k1 + 1 = i or k1 + 1 < i ) by A62, XXREAL_0:1; supposeA63: k1 + 1 = i ; ::_thesis: contradiction then k1 <= i by NAT_1:11; then A64: k1 in dom (f | i) by A24, A38, FINSEQ_1:1; then A65: h /. k1 = (f | i) /. k1 by A7, FINSEQ_4:68 .= f /. k1 by A64, FINSEQ_4:70 ; k1 + 1 <= len f by A2, A15, A63, FINSEQ_1:1; then A66: f /. k1 in LSeg (f,k1) by A38, TOPREAL1:21; (LSeg (f,k1)) /\ (LSeg (f,i)) = {(f /. i)} by A12, A16, A38, A46, A63, TOPREAL1:def_6; then f /. k1 in {(f /. i)} by A5, A26, A27, A43, A60, A66, A65, XBOOLE_0:def_4; then A67: f /. k1 = f /. i by TARSKI:def_1; k1 < i by A63, NAT_1:13; hence contradiction by A2, A8, A45, A67, PARTFUN2:10; ::_thesis: verum end; supposeA68: k1 + 1 < i ; ::_thesis: contradiction then A69: k1 + 1 <= len f by A23, XXREAL_0:2; A70: LSeg (f,k1) misses LSeg (f,i) by A14, A68, TOPREAL1:def_7; k1 <= k1 + 1 by NAT_1:11; then k1 <= i by A68, XXREAL_0:2; then A71: k1 in dom (f | i) by A24, A38, FINSEQ_1:1; then h /. k1 = (f | i) /. k1 by A7, FINSEQ_4:68 .= f /. k1 by A71, FINSEQ_4:70 ; then p in LSeg (f,k1) by A26, A27, A38, A43, A60, A69, TOPREAL1:21; hence contradiction by A5, A70, XBOOLE_0:3; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; supposeA72: ( k1 < i + 1 & k2 < i + 1 ) ; ::_thesis: contradiction then k2 <= i by NAT_1:13; then A73: k2 in dom (f | i) by A24, A41, FINSEQ_1:1; k1 <= i by A72, NAT_1:13; then A74: k1 in dom (f | i) by A24, A38, FINSEQ_1:1; then f . k1 = (f | i) . k1 by A9, FUNCT_1:47 .= h . k1 by A7, A74, FINSEQ_1:def_7 .= (f | i) . k2 by A7, A35, A37, A40, A73, FINSEQ_1:def_7 .= f . k2 by A9, A73, FUNCT_1:47 ; hence contradiction by A8, A36, A37, A40, A45, A44, FUNCT_1:def_4; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; hence h is one-to-one by FUNCT_1:def_4; :: according to TOPREAL1:def_8 ::_thesis: ( 2 <= len h & h is unfolded & h is s.n.c. & h is special ) thus len h >= 2 by A4, A26, A31, XREAL_1:6; ::_thesis: ( h is unfolded & h is s.n.c. & h is special ) thus h is unfolded ::_thesis: ( h is s.n.c. & h is special ) proof let j be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= j or not j + 2 <= len h or (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} ) assume that A75: 1 <= j and A76: j + 2 <= len h ; ::_thesis: (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} A77: 1 <= j + 1 by NAT_1:11; (j + 1) + 1 = j + (1 + 1) ; then j + 1 <= i by A26, A76, XREAL_1:6; then A78: j + 1 in dom (f | i) by A24, A77, FINSEQ_1:1; then A79: h /. (j + 1) = (f | i) /. (j + 1) by A7, FINSEQ_4:68 .= f /. (j + 1) by A78, FINSEQ_4:70 ; (i + 1) + 1 = i + (1 + 1) ; then len h <= i + 2 by A26, NAT_1:11; then j + 2 <= i + 2 by A76, XXREAL_0:2; then j <= i by XREAL_1:6; then A80: j in dom (f | i) by A24, A75, FINSEQ_1:1; then A81: LSeg (h,j) = LSeg ((f | i),j) by A7, A78, TOPREAL3:18 .= LSeg (f,j) by A80, A78, TOPREAL3:17 ; j <= j + 2 by NAT_1:11; then A82: 1 <= j + (1 + 1) by A75, XXREAL_0:2; A83: j + (1 + 1) = (j + 1) + 1 ; i + 1 in Seg (len f) by A3, FINSEQ_1:def_3; then len h <= len f by A26, FINSEQ_1:1; then A84: j + 2 <= len f by A76, XXREAL_0:2; then A85: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A12, A75, TOPREAL1:def_6; now__::_thesis:_(LSeg_(h,j))_/\_(LSeg_(h,(j_+_1)))_=_{(h_/._(j_+_1))} percases ( j + 2 = len h or j + 2 < len h ) by A76, XXREAL_0:1; supposeA86: j + 2 = len h ; ::_thesis: (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} j + 1 <= (j + 1) + 1 by NAT_1:11; then j + 1 <= len h by A76, XXREAL_0:2; then A87: h /. (j + 1) in LSeg (h,j) by A75, TOPREAL1:21; h /. (j + 1) in LSeg (h,(j + 1)) by A76, A77, A83, TOPREAL1:21; then h /. (j + 1) in (LSeg (h,j)) /\ (LSeg (h,(j + 1))) by A87, XBOOLE_0:def_4; then A88: {(h /. (j + 1))} c= (LSeg (h,j)) /\ (LSeg (h,(j + 1))) by ZFMISC_1:31; (LSeg (h,j)) /\ (LSeg (h,(j + 1))) c= {(h /. (j + 1))} by A26, A18, A21, A17, A30, A85, A81, A79, A86, TOPREAL1:6, XBOOLE_1:26; hence (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} by A88, XBOOLE_0:def_10; ::_thesis: verum end; suppose j + 2 < len h ; ::_thesis: (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} then j + (1 + 1) <= i by A26, NAT_1:13; then A89: (j + 1) + 1 in dom (f | i) by A24, A82, FINSEQ_1:1; then LSeg (h,(j + 1)) = LSeg ((f | i),(j + 1)) by A7, A78, TOPREAL3:18 .= LSeg (f,(j + 1)) by A78, A89, TOPREAL3:17 ; hence (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} by A12, A75, A84, A81, A79, TOPREAL1:def_6; ::_thesis: verum end; end; end; hence (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} ; ::_thesis: verum end; thus h is s.n.c. ::_thesis: h is special proof let n, m be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( m <= n + 1 or LSeg (h,n) misses LSeg (h,m) ) assume A90: m > n + 1 ; ::_thesis: LSeg (h,n) misses LSeg (h,m) n <= n + 1 by NAT_1:11; then A91: n <= m by A90, XXREAL_0:2; A92: 1 <= n + 1 by NAT_1:11; A93: LSeg (f,n) misses LSeg (f,m) by A14, A90, TOPREAL1:def_7; now__::_thesis:_(LSeg_(h,n))_/\_(LSeg_(h,m))_=_{} percases ( m + 1 < len h or m + 1 = len h or m + 1 > len h ) by XXREAL_0:1; supposeA94: m + 1 < len h ; ::_thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {} A95: 1 < m by A90, A92, XXREAL_0:2; then A96: 1 <= m + 1 by NAT_1:13; m + 1 <= i by A26, A94, NAT_1:13; then A97: m + 1 in dom (f | i) by A24, A96, FINSEQ_1:1; A98: m <= i by A26, A94, XREAL_1:6; then A99: m in dom (f | i) by A24, A95, FINSEQ_1:1; then A100: LSeg (h,m) = LSeg ((f | i),m) by A7, A97, TOPREAL3:18 .= LSeg (f,m) by A99, A97, TOPREAL3:17 ; now__::_thesis:_(LSeg_(h,n))_/\_(LSeg_(h,m))_=_{} percases ( 0 < n or 0 = n ) ; suppose 0 < n ; ::_thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {} then A101: 0 + 1 <= n by NAT_1:13; n + 1 <= i by A90, A98, XXREAL_0:2; then A102: n + 1 in dom (f | i) by A24, A92, FINSEQ_1:1; n <= i by A91, A98, XXREAL_0:2; then A103: n in dom (f | i) by A24, A101, FINSEQ_1:1; then LSeg (h,n) = LSeg ((f | i),n) by A7, A102, TOPREAL3:18 .= LSeg (f,n) by A103, A102, TOPREAL3:17 ; then LSeg (h,n) misses LSeg (h,m) by A14, A90, A100, TOPREAL1:def_7; hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} by XBOOLE_0:def_7; ::_thesis: verum end; suppose 0 = n ; ::_thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {} then LSeg (h,n) = {} by TOPREAL1:def_3; hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; ::_thesis: verum end; end; end; hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; ::_thesis: verum end; supposeA104: m + 1 = len h ; ::_thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {} A105: (LSeg (f,n)) /\ (LSeg (f,m)) = {} by A93, XBOOLE_0:def_7; now__::_thesis:_{}_=_(LSeg_(h,n))_/\_(LSeg_(h,m)) percases ( 0 < n or 0 = n ) ; suppose 0 < n ; ::_thesis: {} = (LSeg (h,n)) /\ (LSeg (h,m)) then 0 + 1 <= n by NAT_1:13; then A106: n in dom (f | i) by A24, A26, A91, A104, FINSEQ_1:1; A107: n + 1 in dom (f | i) by A24, A26, A90, A92, A104, FINSEQ_1:1; then LSeg (h,n) = LSeg ((f | i),n) by A7, A106, TOPREAL3:18 .= LSeg (f,n) by A106, A107, TOPREAL3:17 ; hence {} = (LSeg (h,m)) /\ ((LSeg (f,m)) /\ (LSeg (h,n))) by A105 .= ((LSeg (h,m)) /\ (LSeg (f,m))) /\ (LSeg (h,n)) by XBOOLE_1:16 .= (LSeg (h,n)) /\ (LSeg (h,m)) by A26, A18, A21, A17, A30, A104, TOPREAL1:6, XBOOLE_1:28 ; ::_thesis: verum end; suppose 0 = n ; ::_thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {} then LSeg (h,n) = {} by TOPREAL1:def_3; hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; ::_thesis: verum end; end; end; hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; ::_thesis: verum end; suppose m + 1 > len h ; ::_thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {} then LSeg (h,m) = {} by TOPREAL1:def_3; hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; ::_thesis: verum end; end; end; hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum end; let n be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= n or not n + 1 <= len h or (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) assume that A108: 1 <= n and A109: n + 1 <= len h ; ::_thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) set p3 = h /. n; set p4 = h /. (n + 1); now__::_thesis:_(_(h_/._n)_`1_=_(h_/._(n_+_1))_`1_or_(h_/._n)_`2_=_(h_/._(n_+_1))_`2_) percases ( n + 1 = len h or n + 1 < len h ) by A109, XXREAL_0:1; supposeA110: n + 1 = len h ; ::_thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) A111: i in dom (f | i) by A4, A24, FINSEQ_1:1; then A112: h /. n = (f | i) /. i by A7, A26, A110, FINSEQ_4:68 .= f /. i by A111, FINSEQ_4:70 ; now__::_thesis:_(_(h_/._n)_`1_=_(h_/._(n_+_1))_`1_or_(h_/._n)_`2_=_(h_/._(n_+_1))_`2_) percases ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A4, A13, A16, TOPREAL1:def_5; supposeA113: (f /. i) `1 = (f /. (i + 1)) `1 ; ::_thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) then A114: (f /. i) `2 <> (f /. (i + 1)) `2 by A20, TOPREAL3:6; now__::_thesis:_(_(h_/._n)_`1_=_(h_/._(n_+_1))_`1_or_(h_/._n)_`2_=_(h_/._(n_+_1))_`2_) percases ( (f /. i) `2 < (f /. (i + 1)) `2 or (f /. (i + 1)) `2 < (f /. i) `2 ) by A114, XXREAL_0:1; suppose (f /. i) `2 < (f /. (i + 1)) `2 ; ::_thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) then p in { p11 where p11 is Point of (TOP-REAL 2) : ( p11 `1 = (f /. i) `1 & (f /. i) `2 <= p11 `2 & p11 `2 <= (f /. (i + 1)) `2 ) } by A5, A19, A22, A113, TOPREAL3:9; then ex p11 being Point of (TOP-REAL 2) st ( p = p11 & p11 `1 = (f /. i) `1 & (f /. i) `2 <= p11 `2 & p11 `2 <= (f /. (i + 1)) `2 ) ; hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) by A7, A25, A26, A110, A112, FINSEQ_4:67; ::_thesis: verum end; suppose (f /. (i + 1)) `2 < (f /. i) `2 ; ::_thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) then p in { p22 where p22 is Point of (TOP-REAL 2) : ( p22 `1 = (f /. i) `1 & (f /. (i + 1)) `2 <= p22 `2 & p22 `2 <= (f /. i) `2 ) } by A5, A19, A22, A113, TOPREAL3:9; then ex p11 being Point of (TOP-REAL 2) st ( p = p11 & p11 `1 = (f /. i) `1 & (f /. (i + 1)) `2 <= p11 `2 & p11 `2 <= (f /. i) `2 ) ; hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) by A7, A25, A26, A110, A112, FINSEQ_4:67; ::_thesis: verum end; end; end; hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) ; ::_thesis: verum end; supposeA115: (f /. i) `2 = (f /. (i + 1)) `2 ; ::_thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) then A116: (f /. i) `1 <> (f /. (i + 1)) `1 by A20, TOPREAL3:6; now__::_thesis:_(_(h_/._n)_`1_=_(h_/._(n_+_1))_`1_or_(h_/._n)_`2_=_(h_/._(n_+_1))_`2_) percases ( (f /. i) `1 < (f /. (i + 1)) `1 or (f /. (i + 1)) `1 < (f /. i) `1 ) by A116, XXREAL_0:1; suppose (f /. i) `1 < (f /. (i + 1)) `1 ; ::_thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) then p in { p11 where p11 is Point of (TOP-REAL 2) : ( p11 `2 = (f /. i) `2 & (f /. i) `1 <= p11 `1 & p11 `1 <= (f /. (i + 1)) `1 ) } by A5, A19, A22, A115, TOPREAL3:10; then ex p11 being Point of (TOP-REAL 2) st ( p = p11 & p11 `2 = (f /. i) `2 & (f /. i) `1 <= p11 `1 & p11 `1 <= (f /. (i + 1)) `1 ) ; hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) by A7, A25, A26, A110, A112, FINSEQ_4:67; ::_thesis: verum end; suppose (f /. (i + 1)) `1 < (f /. i) `1 ; ::_thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) then p in { p22 where p22 is Point of (TOP-REAL 2) : ( p22 `2 = (f /. i) `2 & (f /. (i + 1)) `1 <= p22 `1 & p22 `1 <= (f /. i) `1 ) } by A5, A19, A22, A115, TOPREAL3:10; then ex p11 being Point of (TOP-REAL 2) st ( p = p11 & p11 `2 = (f /. i) `2 & (f /. (i + 1)) `1 <= p11 `1 & p11 `1 <= (f /. i) `1 ) ; hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) by A7, A25, A26, A110, A112, FINSEQ_4:67; ::_thesis: verum end; end; end; hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) ; ::_thesis: verum end; end; end; hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) ; ::_thesis: verum end; supposeA117: n + 1 < len h ; ::_thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) A118: 1 <= n + 1 by A108, NAT_1:13; n + 1 <= i by A26, A117, NAT_1:13; then A119: n + 1 in dom (f | i) by A24, A118, FINSEQ_1:1; then h /. (n + 1) = (f | i) /. (n + 1) by A7, FINSEQ_4:68; then A120: h /. (n + 1) = f /. (n + 1) by A119, FINSEQ_4:70; n <= i by A26, A117, XREAL_1:6; then A121: n in dom (f | i) by A24, A108, FINSEQ_1:1; then h /. n = (f | i) /. n by A7, FINSEQ_4:68; then A122: h /. n = f /. n by A121, FINSEQ_4:70; n + 1 <= len f by A26, A16, A109, XXREAL_0:2; hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) by A13, A108, A122, A120, TOPREAL1:def_5; ::_thesis: verum end; end; end; hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) ; ::_thesis: verum end; A123: 1 in dom (f | i) by A4, A24, FINSEQ_1:1; then h /. 1 = (f | i) /. 1 by A7, FINSEQ_4:68 .= f /. 1 by A123, FINSEQ_4:70 ; hence A124: ( h /. 1 = f /. 1 & h /. (len h) = p ) by A7, A25, A26, FINSEQ_4:67; ::_thesis: ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),p)) ) set Mf = { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ; set Mv = { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } ; set Mh = { (LSeg (h,m)) where m is Element of NAT : ( 1 <= m & m + 1 <= len h ) } ; A125: Seg (len (f | i)) = dom (f | i) by FINSEQ_1:def_3; thus L~ h is_S-P_arc_joining f /. 1,p by A32, A124, Def1; ::_thesis: ( L~ h c= L~ f & L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),p)) ) A126: now__::_thesis:_for_x_being_set_st_x_in_L~_h_holds_ (_x_in_L~_f_&_x_in_(L~_(f_|_i))_\/_(LSeg_((f_/._i),p))_) let x be set ; ::_thesis: ( x in L~ h implies ( x in L~ f & x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) ) ) assume x in L~ h ; ::_thesis: ( x in L~ f & x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) ) then consider X being set such that A127: x in X and A128: X in { (LSeg (h,m)) where m is Element of NAT : ( 1 <= m & m + 1 <= len h ) } by TARSKI:def_4; consider k being Element of NAT such that A129: X = LSeg (h,k) and A130: 1 <= k and A131: k + 1 <= len h by A128; A132: k + 1 <= len f by A26, A16, A131, XXREAL_0:2; now__::_thesis:_(_x_in_L~_f_&_x_in_(L~_(f_|_i))_\/_(LSeg_((f_/._i),p))_) percases ( k + 1 = len h or k + 1 < len h ) by A131, XXREAL_0:1; supposeA133: k + 1 = len h ; ::_thesis: ( x in L~ f & x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) ) then A134: LSeg (f,k) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A26, A16, A130; LSeg (h,i) c= LSeg (f,i) by A5, A18, A21, A30, TOPREAL1:6; hence x in L~ f by A26, A127, A129, A133, A134, TARSKI:def_4; ::_thesis: x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) thus x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) by A26, A30, A127, A129, A133, XBOOLE_0:def_3; ::_thesis: verum end; supposeA135: k + 1 < len h ; ::_thesis: ( x in L~ f & x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) ) then A136: k + 1 <= len (f | i) by A25, A26, NAT_1:13; A137: k + 1 <= i by A26, A135, NAT_1:13; k <= k + 1 by NAT_1:11; then k <= i by A137, XXREAL_0:2; then A138: k in dom (f | i) by A24, A130, FINSEQ_1:1; 1 <= k + 1 by A130, NAT_1:13; then A139: k + 1 in dom (f | i) by A24, A137, FINSEQ_1:1; then A140: X = LSeg ((f | i),k) by A7, A129, A138, TOPREAL3:18 .= LSeg (f,k) by A139, A138, TOPREAL3:17 ; then X in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A130, A132; hence x in L~ f by A127, TARSKI:def_4; ::_thesis: x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) X = LSeg ((f | i),k) by A139, A138, A140, TOPREAL3:17; then X in { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } by A130, A136; then x in union { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } by A127, TARSKI:def_4; hence x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence ( x in L~ f & x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) ) ; ::_thesis: verum end; thus L~ h c= L~ f ::_thesis: L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),p)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ h or x in L~ f ) assume x in L~ h ; ::_thesis: x in L~ f hence x in L~ f by A126; ::_thesis: verum end; A141: i <= i + 1 by NAT_1:11; thus L~ h c= (L~ (f | i)) \/ (LSeg ((f /. i),p)) :: according to XBOOLE_0:def_10 ::_thesis: (L~ (f | i)) \/ (LSeg ((f /. i),p)) c= L~ h proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ h or x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) ) assume x in L~ h ; ::_thesis: x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) hence x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) by A126; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) or x in L~ h ) assume A142: x in (L~ (f | i)) \/ (LSeg ((f /. i),p)) ; ::_thesis: x in L~ h now__::_thesis:_x_in_L~_h percases ( x in L~ (f | i) or x in LSeg ((f /. i),p) ) by A142, XBOOLE_0:def_3; suppose x in L~ (f | i) ; ::_thesis: x in L~ h then consider X being set such that A143: x in X and A144: X in { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } by TARSKI:def_4; consider k being Element of NAT such that A145: X = LSeg ((f | i),k) and A146: 1 <= k and A147: k + 1 <= len (f | i) by A144; A148: k + 1 <= len h by A25, A26, A141, A147, XXREAL_0:2; k <= k + 1 by NAT_1:11; then k <= len (f | i) by A147, XXREAL_0:2; then A149: k in Seg (len (f | i)) by A146, FINSEQ_1:1; 1 <= k + 1 by NAT_1:11; then k + 1 in Seg (len (f | i)) by A147, FINSEQ_1:1; then X = LSeg (h,k) by A7, A125, A145, A149, TOPREAL3:18; then X in { (LSeg (h,m)) where m is Element of NAT : ( 1 <= m & m + 1 <= len h ) } by A146, A148; hence x in L~ h by A143, TARSKI:def_4; ::_thesis: verum end; supposeA150: x in LSeg ((f /. i),p) ; ::_thesis: x in L~ h LSeg (h,i) in { (LSeg (h,m)) where m is Element of NAT : ( 1 <= m & m + 1 <= len h ) } by A4, A26; hence x in L~ h by A30, A150, TARSKI:def_4; ::_thesis: verum end; end; end; hence x in L~ h ; ::_thesis: verum 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))) ) proof let f, h be FinSequence of (TOP-REAL 2); ::_thesis: ( 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)*> implies ( 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))) ) ) set p1 = f /. 1; set p = f /. 2; assume that A1: f /. 2 <> f /. 1 and A2: f is being_S-Seq and A3: (f /. 2) `2 = (f /. 1) `2 and A4: h = <*(f /. 1),|[((((f /. 1) `1) + ((f /. 2) `1)) / 2),((f /. 1) `2)]|,(f /. 2)*> ; ::_thesis: ( 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))) ) A5: (f /. 1) `1 <> (f /. 2) `1 by A1, A3, TOPREAL3:6; hence A6: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. 2 ) by A3, A4, TOPREAL3:37; ::_thesis: ( 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))) ) A7: (LSeg ((f /. 1),|[((((f /. 1) `1) + ((f /. 2) `1)) / 2),((f /. 1) `2)]|)) \/ (LSeg (|[((((f /. 1) `1) + ((f /. 2) `1)) / 2),((f /. 1) `2)]|,(f /. 2))) = LSeg ((f /. 1),(f /. 2)) by A3, A5, TOPREAL1:5, TOPREAL3:13; set M = { (LSeg ((f | 2),k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | 2) ) } ; A8: Seg (len f) = dom f by FINSEQ_1:def_3; A9: L~ h = (LSeg ((f /. 1),|[((((f /. 1) `1) + ((f /. 2) `1)) / 2),((f /. 1) `2)]|)) \/ (LSeg (|[((((f /. 1) `1) + ((f /. 2) `1)) / 2),((f /. 1) `2)]|,(f /. 2))) by A4, TOPREAL3:16; A10: len f >= 2 by A2, TOPREAL1:def_8; then A11: 1 + 1 in Seg (len f) by FINSEQ_1:1; then A12: LSeg (f,1) = LSeg ((f /. 1),(f /. 2)) by A10, TOPREAL1:def_3; Seg 2 c= Seg (len f) by A10, FINSEQ_1:5; then ( f | 2 = f | (Seg 2) & (dom f) /\ (Seg 2) = Seg 2 ) by A8, FINSEQ_1:def_15, XBOOLE_1:28; then A13: dom (f | 2) = Seg 2 by RELAT_1:61; then A14: ( 1 in dom (f | 2) & 2 in dom (f | 2) ) by FINSEQ_1:1; thus A15: L~ h is_S-P_arc_joining f /. 1,f /. 2 by A6, Def1; ::_thesis: ( 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))) ) A16: (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) c= L~ h proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) or x in L~ h ) assume A17: x in (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) ; ::_thesis: x in L~ h now__::_thesis:_x_in_L~_h percases ( x in L~ (f | 2) or x in LSeg ((f /. 2),(f /. 2)) ) by A17, XBOOLE_0:def_3; suppose x in L~ (f | 2) ; ::_thesis: x in L~ h then consider X being set such that A18: x in X and A19: X in { (LSeg ((f | 2),k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | 2) ) } by TARSKI:def_4; consider m being Element of NAT such that A20: X = LSeg ((f | 2),m) and A21: 1 <= m and A22: m + 1 <= len (f | 2) by A19; (len (f | 2)) - 1 = (1 + 1) - 1 by A13, FINSEQ_1:def_3 .= 1 ; then (m + 1) - 1 <= 1 by A22, XREAL_1:9; then m = 1 by A21, XXREAL_0:1; hence x in L~ h by A11, A12, A9, A7, A14, A18, A20, TOPREAL3:17; ::_thesis: verum end; suppose x in LSeg ((f /. 2),(f /. 2)) ; ::_thesis: x in L~ h then A23: x in {(f /. 2)} by RLTOPSP1:70; f /. 2 in L~ h by A15, Th3; hence x in L~ h by A23, TARSKI:def_1; ::_thesis: verum end; end; end; hence x in L~ h ; ::_thesis: verum end; LSeg (f,1) c= L~ f by TOPREAL3:19; hence L~ h c= L~ f by A4, A12, A7, TOPREAL3:16; ::_thesis: ( L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),(f /. 2))) & L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) ) len f >= 1 by A10, XXREAL_0:2; then Seg 1 c= Seg (len f) by FINSEQ_1:5; then ( f | 1 = f | (Seg 1) & (dom f) /\ (Seg 1) = Seg 1 ) by A8, FINSEQ_1:def_15, XBOOLE_1:28; then dom (f | 1) = Seg 1 by RELAT_1:61; then len (f | 1) = 1 by FINSEQ_1:def_3; then L~ (f | 1) = {} by TOPREAL1:22; hence L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),(f /. 2))) by A3, A5, A9, TOPREAL1:5, TOPREAL3:13; ::_thesis: L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) A24: L~ (f | 2) c= (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) by XBOOLE_1:7; A25: 1 + 1 <= len (f | 2) by A13, FINSEQ_1:def_3; LSeg ((f | 2),1) = LSeg ((f /. 1),(f /. 2)) by A11, A12, A14, TOPREAL3:17; then LSeg ((f /. 1),(f /. 2)) in { (LSeg ((f | 2),k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | 2) ) } by A25; then L~ h c= L~ (f | 2) by A9, A7, ZFMISC_1:74; then L~ h c= (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) by A24, XBOOLE_1:1; hence L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) by A16, XBOOLE_0:def_10; ::_thesis: verum 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))) ) proof let f, h be FinSequence of (TOP-REAL 2); ::_thesis: ( 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)*> implies ( 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))) ) ) set p1 = f /. 1; set p = f /. 2; assume that A1: f /. 2 <> f /. 1 and A2: f is being_S-Seq and A3: (f /. 2) `1 = (f /. 1) `1 and A4: h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + ((f /. 2) `2)) / 2)]|,(f /. 2)*> ; ::_thesis: ( 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))) ) A5: (f /. 1) `2 <> (f /. 2) `2 by A1, A3, TOPREAL3:6; hence A6: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. 2 ) by A3, A4, TOPREAL3:36; ::_thesis: ( 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))) ) A7: (LSeg ((f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + ((f /. 2) `2)) / 2)]|)) \/ (LSeg (|[((f /. 1) `1),((((f /. 1) `2) + ((f /. 2) `2)) / 2)]|,(f /. 2))) = LSeg ((f /. 1),(f /. 2)) by A3, A5, TOPREAL1:5, TOPREAL3:14; set M = { (LSeg ((f | 2),k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | 2) ) } ; A8: Seg (len f) = dom f by FINSEQ_1:def_3; A9: L~ h = (LSeg ((f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + ((f /. 2) `2)) / 2)]|)) \/ (LSeg (|[((f /. 1) `1),((((f /. 1) `2) + ((f /. 2) `2)) / 2)]|,(f /. 2))) by A4, TOPREAL3:16; A10: len f >= 1 + 1 by A2, TOPREAL1:def_8; then A11: LSeg (f,1) = LSeg ((f /. 1),(f /. 2)) by TOPREAL1:def_3; Seg 2 c= Seg (len f) by A10, FINSEQ_1:5; then ( f | 2 = f | (Seg 2) & (dom f) /\ (Seg 2) = Seg 2 ) by A8, FINSEQ_1:def_15, XBOOLE_1:28; then A12: dom (f | 2) = Seg 2 by RELAT_1:61; then A13: ( 1 in dom (f | 2) & 2 in dom (f | 2) ) by FINSEQ_1:1; thus A14: L~ h is_S-P_arc_joining f /. 1,f /. 2 by A6, Def1; ::_thesis: ( 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))) ) A15: (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) c= L~ h proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) or x in L~ h ) assume A16: x in (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) ; ::_thesis: x in L~ h now__::_thesis:_x_in_L~_h percases ( x in L~ (f | 2) or x in LSeg ((f /. 2),(f /. 2)) ) by A16, XBOOLE_0:def_3; suppose x in L~ (f | 2) ; ::_thesis: x in L~ h then consider X being set such that A17: x in X and A18: X in { (LSeg ((f | 2),k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | 2) ) } by TARSKI:def_4; consider m being Element of NAT such that A19: X = LSeg ((f | 2),m) and A20: 1 <= m and A21: m + 1 <= len (f | 2) by A18; (len (f | 2)) - 1 = (1 + 1) - 1 by A12, FINSEQ_1:def_3 .= 1 ; then (m + 1) - 1 <= 1 by A21, XREAL_1:9; then m = 1 by A20, XXREAL_0:1; hence x in L~ h by A10, A11, A9, A7, A13, A17, A19, TOPREAL3:17; ::_thesis: verum end; suppose x in LSeg ((f /. 2),(f /. 2)) ; ::_thesis: x in L~ h then A22: x in {(f /. 2)} by RLTOPSP1:70; f /. 2 in L~ h by A14, Th3; hence x in L~ h by A22, TARSKI:def_1; ::_thesis: verum end; end; end; hence x in L~ h ; ::_thesis: verum end; LSeg (f,1) c= L~ f by TOPREAL3:19; hence L~ h c= L~ f by A4, A11, A7, TOPREAL3:16; ::_thesis: ( L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),(f /. 2))) & L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) ) len f >= 1 by A10, XXREAL_0:2; then Seg 1 c= Seg (len f) by FINSEQ_1:5; then ( f | 1 = f | (Seg 1) & (dom f) /\ (Seg 1) = Seg 1 ) by A8, FINSEQ_1:def_15, XBOOLE_1:28; then dom (f | 1) = Seg 1 by RELAT_1:61; then len (f | 1) = 1 by FINSEQ_1:def_3; then L~ (f | 1) = {} by TOPREAL1:22; hence L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),(f /. 2))) by A3, A5, A9, TOPREAL1:5, TOPREAL3:14; ::_thesis: L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) A23: L~ (f | 2) c= (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) by XBOOLE_1:7; A24: 1 + 1 <= len (f | 2) by A12, FINSEQ_1:def_3; LSeg ((f | 2),1) = LSeg ((f /. 1),(f /. 2)) by A10, A11, A13, TOPREAL3:17; then LSeg ((f /. 1),(f /. 2)) in { (LSeg ((f | 2),k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | 2) ) } by A24; then L~ h c= L~ (f | 2) by A9, A7, ZFMISC_1:74; then L~ h c= (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) by A23, XBOOLE_1:1; hence L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) by A15, XBOOLE_0:def_10; ::_thesis: verum 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))) ) proof let f, h be FinSequence of (TOP-REAL 2); ::_thesis: 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))) ) let i be Element of NAT ; ::_thesis: ( f is being_S-Seq & i > 2 & i in dom f & h = f | i implies ( 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))) ) ) assume that A1: ( f is being_S-Seq & i > 2 ) and A2: i in dom f and A3: h = f | i ; ::_thesis: ( 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))) ) A4: Seg (len f) = dom f by FINSEQ_1:def_3; then i <= len f by A2, FINSEQ_1:1; then A5: Seg i c= Seg (len f) by FINSEQ_1:5; h = f | (Seg i) by A3, FINSEQ_1:def_15; then dom h = (Seg (len f)) /\ (Seg i) by A4, RELAT_1:61; then A6: dom h = Seg i by A5, XBOOLE_1:28; 1 <= i by A2, A4, FINSEQ_1:1; then A7: ( 1 in dom h & i in dom h ) by A6, FINSEQ_1:1; len h = i by A6, FINSEQ_1:def_3; hence ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. i ) by A1, A2, A3, A7, FINSEQ_4:70, TOPREAL3:33; ::_thesis: ( 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))) ) hence ( L~ h is_S-P_arc_joining f /. 1,f /. i & L~ h c= L~ f ) by A3, Def1, TOPREAL3:20; ::_thesis: L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. i))) then f /. i in L~ (f | i) by A3, Th3; then ( LSeg ((f /. i),(f /. i)) = {(f /. i)} & {(f /. i)} c= L~ (f | i) ) by RLTOPSP1:70, ZFMISC_1:31; hence L~ h = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. i))) by A3, XBOOLE_1:12; ::_thesis: verum 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)) ) proof let p be Point of (TOP-REAL 2); ::_thesis: 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)) ) let f be FinSequence of (TOP-REAL 2); ::_thesis: 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)) ) let n be Element of NAT ; ::_thesis: ( p <> f /. 1 & f is being_S-Seq & p in LSeg (f,n) implies 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)) ) ) set p1 = f /. 1; set q = f /. n; assume that A1: p <> f /. 1 and A2: f is being_S-Seq and A3: p in LSeg (f,n) ; ::_thesis: 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)) ) A4: f is special by A2, TOPREAL1:def_8; A5: n <= n + 1 by NAT_1:11; A6: now__::_thesis:_(_n_in_dom_f_&_n_+_1_in_dom_f_) assume A7: ( not n in dom f or not n + 1 in dom f ) ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( not n in dom f or not n + 1 in dom f ) by A7; suppose not n in dom f ; ::_thesis: contradiction then ( not 1 <= n or not n <= len f ) by FINSEQ_3:25; then ( not 1 <= n or not n + 1 <= len f ) by A5, XXREAL_0:2; hence contradiction by A3, TOPREAL1:def_3; ::_thesis: verum end; suppose not n + 1 in dom f ; ::_thesis: contradiction then ( not 1 <= n + 1 or not n + 1 <= len f ) by FINSEQ_3:25; hence contradiction by A3, NAT_1:11, TOPREAL1:def_3; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; A8: f is one-to-one by A2, TOPREAL1:def_8; A9: Seg (len f) = dom f by FINSEQ_1:def_3; then A10: 1 <= n by A6, FINSEQ_1:1; A11: n + 1 <= len f by A6, A9, FINSEQ_1:1; A12: n <= len f by A6, A9, FINSEQ_1:1; now__::_thesis:_(_(_f_/._n_=_p_&_f_/._(n_+_1)_=_p_&_contradiction_)_or_(_f_/._n_=_p_&_f_/._(n_+_1)_<>_p_&_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))_)_)_or_(_f_/._n_<>_p_&_f_/._(n_+_1)_=_p_&_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))_)_)_or_(_f_/._n_<>_p_&_f_/._(n_+_1)_<>_p_&_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))_)_)_) percases ( ( f /. n = p & f /. (n + 1) = p ) or ( f /. n = p & f /. (n + 1) <> p ) or ( f /. n <> p & f /. (n + 1) = p ) or ( f /. n <> p & f /. (n + 1) <> p ) ) ; case ( f /. n = p & f /. (n + 1) = p ) ; ::_thesis: contradiction then n + 1 = n by A6, A8, PARTFUN2:10; hence contradiction ; ::_thesis: verum end; caseA13: ( f /. n = p & f /. (n + 1) <> p ) ; ::_thesis: 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)) ) then 1 < n by A1, A10, XXREAL_0:1; then A14: 1 + 1 <= n by NAT_1:13; now__::_thesis:_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))_) percases ( n = 1 + 1 or n > 2 ) by A14, XXREAL_0:1; supposeA15: n = 1 + 1 ; ::_thesis: 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)) ) now__::_thesis:_ex_h_being_FinSequence_of_the_carrier_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))_) percases ( (f /. 1) `1 = p `1 or (f /. 1) `2 = p `2 ) by A4, A12, A13, A15, TOPREAL1:def_5; supposeA16: (f /. 1) `1 = p `1 ; ::_thesis: ex h being FinSequence of the carrier 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)) ) take h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|,p*>; ::_thesis: ( 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)) ) thus ( 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)) ) by A1, A2, A13, A15, A16, Th15; ::_thesis: verum end; supposeA17: (f /. 1) `2 = p `2 ; ::_thesis: ex h being FinSequence of the carrier 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)) ) take h = <*(f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p*>; ::_thesis: ( 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)) ) thus ( 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)) ) by A1, A2, A13, A15, A17, Th14; ::_thesis: verum end; end; end; hence 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)) ) ; ::_thesis: verum end; supposeA18: n > 2 ; ::_thesis: ex h being FinSequence of the carrier 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)) ) take h = f | n; ::_thesis: ( 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)) ) thus ( 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)) ) by A2, A6, A13, A18, Th16; ::_thesis: verum end; end; end; hence 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)) ) ; ::_thesis: verum end; caseA19: ( f /. n <> p & f /. (n + 1) = p ) ; ::_thesis: 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)) ) now__::_thesis:_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))_) percases ( n = 1 or 1 < n ) by A10, XXREAL_0:1; supposeA20: n = 1 ; ::_thesis: 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)) ) now__::_thesis:_ex_h_being_FinSequence_of_the_carrier_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))_) percases ( (f /. 1) `1 = p `1 or (f /. 1) `2 = p `2 ) by A4, A11, A19, A20, TOPREAL1:def_5; supposeA21: (f /. 1) `1 = p `1 ; ::_thesis: ex h being FinSequence of the carrier 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)) ) take h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|,p*>; ::_thesis: ( 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)) ) thus ( 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)) ) by A2, A19, A20, A21, Th15; ::_thesis: verum end; supposeA22: (f /. 1) `2 = p `2 ; ::_thesis: ex h being FinSequence of the carrier 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)) ) take h = <*(f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p*>; ::_thesis: ( 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)) ) thus ( 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)) ) by A2, A19, A20, A22, Th14; ::_thesis: verum end; end; end; hence 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)) ) ; ::_thesis: verum end; supposeA23: 1 < n ; ::_thesis: ex h being FinSequence of the carrier 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)) ) take h = f | (n + 1); ::_thesis: ( 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)) ) 1 + 1 < n + 1 by A23, XREAL_1:6; hence ( 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)) ) by A2, A6, A19, Th16, TOPREAL3:38; ::_thesis: verum end; end; end; hence 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)) ) ; ::_thesis: verum end; caseA24: ( f /. n <> p & f /. (n + 1) <> p ) ; ::_thesis: 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)) ) now__::_thesis:_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))_) percases ( n = 1 or 1 < n ) by A10, XXREAL_0:1; supposeA25: n = 1 ; ::_thesis: 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)) ) set q1 = f /. (1 + 1); A26: len f >= 1 + 1 by A2, TOPREAL1:def_8; then A27: LSeg (f,n) = LSeg ((f /. 1),(f /. (1 + 1))) by A25, TOPREAL1:def_3; now__::_thesis:_ex_h_being_FinSequence_of_the_carrier_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))_) percases ( (f /. 1) `1 = (f /. (1 + 1)) `1 or (f /. 1) `2 = (f /. (1 + 1)) `2 ) by A4, A26, TOPREAL1:def_5; supposeA28: (f /. 1) `1 = (f /. (1 + 1)) `1 ; ::_thesis: ex h being FinSequence of the carrier 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)) ) take h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|,p*>; ::_thesis: ( 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)) ) ( (f /. 1) `1 <= p `1 & p `1 <= (f /. (1 + 1)) `1 ) by A3, A27, A28, TOPREAL1:3; then (f /. 1) `1 = p `1 by A28, XXREAL_0:1; hence ( 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)) ) by A1, A2, A3, A25, Th12; ::_thesis: verum end; supposeA29: (f /. 1) `2 = (f /. (1 + 1)) `2 ; ::_thesis: ex h being FinSequence of the carrier 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)) ) take h = <*(f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p*>; ::_thesis: ( 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)) ) ( (f /. 1) `2 <= p `2 & p `2 <= (f /. (1 + 1)) `2 ) by A3, A27, A29, TOPREAL1:4; then (f /. 1) `2 = p `2 by A29, XXREAL_0:1; hence ( 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)) ) by A1, A2, A3, A25, Th11; ::_thesis: verum end; end; end; hence 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)) ) ; ::_thesis: verum end; supposeA30: 1 < n ; ::_thesis: ex h being FinSequence of the carrier 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)) ) take h = (f | n) ^ <*p*>; ::_thesis: ( 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)) ) thus ( 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)) ) by A2, A3, A6, A24, A30, Th13; ::_thesis: verum end; end; end; hence 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)) ) ; ::_thesis: verum end; end; end; hence 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)) ) ; ::_thesis: verum 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 ) proof let p be Point of (TOP-REAL 2); ::_thesis: 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 ) let f be FinSequence of (TOP-REAL 2); ::_thesis: ( p <> f /. 1 & f is being_S-Seq & p in L~ f implies 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 ) ) set M = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; set p1 = f /. 1; assume that A1: ( p <> f /. 1 & f is being_S-Seq ) and A2: p in L~ f ; ::_thesis: 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 ) consider X being set such that A3: p in X and A4: X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A2, TARSKI:def_4; consider n being Element of NAT such that A5: X = LSeg (f,n) and 1 <= n and n + 1 <= len f by A4; consider h being FinSequence of (TOP-REAL 2) such that A6: ( 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 ) and L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) by A1, A3, A5, Th17; take h ; ::_thesis: ( 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 ) thus ( 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 ) by A6; ::_thesis: verum 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)) ) proof let p be Point of (TOP-REAL 2); ::_thesis: 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)) ) let f, h be FinSequence of (TOP-REAL 2); ::_thesis: 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)) ) let r be Real; ::_thesis: 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)) ) let u be Point of (Euclid 2); ::_thesis: ( ( ( 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*> implies ( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) ) set p1 = f /. 1; set p2 = f /. (len f); assume A1: ( ( 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 ) ) ; ::_thesis: ( not f /. (len f) in Ball (u,r) or not p in Ball (u,r) or not f is being_S-Seq or not (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} or not h = f ^ <*p*> or ( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) ) assume that A2: ( f /. (len f) in Ball (u,r) & p in Ball (u,r) ) and A3: f is being_S-Seq and A4: (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} and A5: h = f ^ <*p*> ; ::_thesis: ( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) A6: not p in L~ f by A1, A4, TOPREAL3:40; A7: f is one-to-one by A3, TOPREAL1:def_8; A8: f is unfolded by A3, TOPREAL1:def_8; A9: f is one-to-one by A3, TOPREAL1:def_8; A10: f is s.n.c. by A3, TOPREAL1:def_8; A11: Seg (len h) = dom h by FINSEQ_1:def_3; set Mf = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; set Mh = { (LSeg (h,m)) where m is Element of NAT : ( 1 <= m & m + 1 <= len h ) } ; A12: Seg (len f) = dom f by FINSEQ_1:def_3; A13: 2 <= len f by A3, TOPREAL1:def_8; then A14: 1 <= len f by XXREAL_0:2; then A15: len f in dom f by A12, FINSEQ_1:1; then A16: h /. (len f) = f /. (len f) by A5, FINSEQ_4:68; A17: len h = (len f) + (len <*p*>) by A5, FINSEQ_1:22 .= (len f) + 1 by FINSEQ_1:39 ; then A18: h /. (len h) = p by A5, FINSEQ_4:67; then A19: LSeg (h,(len f)) = LSeg ((f /. (len f)),p) by A17, A14, A16, TOPREAL1:def_3; A20: f is special by A3, TOPREAL1:def_8; thus A21: h is being_S-Seq ::_thesis: ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) proof now__::_thesis:_for_x,_y_being_set_holds_ (_not_x_in_dom_h_or_not_y_in_dom_h_or_not_h_._x_=_h_._y_or_not_x_<>_y_) set Z = { m where m is Element of NAT : ( 1 <= m & m <= len h ) } ; given x, y being set such that A22: x in dom h and A23: y in dom h and A24: h . x = h . y and A25: x <> y ; ::_thesis: contradiction y in { m where m is Element of NAT : ( 1 <= m & m <= len h ) } by A11, A23, FINSEQ_1:def_1; then consider k2 being Element of NAT such that A26: k2 = y and A27: 1 <= k2 and A28: k2 <= len h ; x in { m where m is Element of NAT : ( 1 <= m & m <= len h ) } by A11, A22, FINSEQ_1:def_1; then consider k1 being Element of NAT such that A29: k1 = x and A30: 1 <= k1 and A31: k1 <= len h ; A32: h /. k1 = h . y by A22, A24, A29, PARTFUN1:def_6 .= h /. k2 by A23, A26, PARTFUN1:def_6 ; now__::_thesis:_contradiction percases ( ( k1 = (len f) + 1 & k2 = (len f) + 1 ) or ( k1 = (len f) + 1 & k2 < (len f) + 1 ) or ( k1 < (len f) + 1 & k2 = (len f) + 1 ) or ( k1 < (len f) + 1 & k2 < (len f) + 1 ) ) by A17, A31, A28, XXREAL_0:1; suppose ( k1 = (len f) + 1 & k2 = (len f) + 1 ) ; ::_thesis: contradiction hence contradiction by A25, A29, A26; ::_thesis: verum end; supposeA33: ( k1 = (len f) + 1 & k2 < (len f) + 1 ) ; ::_thesis: contradiction then A34: k2 + 1 <= k1 by NAT_1:13; now__::_thesis:_contradiction percases ( k2 + 1 = k1 or k2 + 1 < k1 ) by A34, XXREAL_0:1; suppose k2 + 1 = k1 ; ::_thesis: contradiction hence contradiction by A1, A5, A16, A32, A33, FINSEQ_4:67; ::_thesis: verum end; suppose k2 + 1 < k1 ; ::_thesis: contradiction then A35: k2 < ((len f) + 1) - 1 by A33, XREAL_1:20; then k2 in dom f by A12, A27, FINSEQ_1:1; then h /. k2 = f /. k2 by A5, FINSEQ_4:68; hence contradiction by A5, A13, A6, A27, A32, A33, A35, FINSEQ_4:67, TOPREAL3:39; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; supposeA36: ( k1 < (len f) + 1 & k2 = (len f) + 1 ) ; ::_thesis: contradiction then A37: k1 + 1 <= k2 by NAT_1:13; now__::_thesis:_contradiction percases ( k1 + 1 = k2 or k1 + 1 < k2 ) by A37, XXREAL_0:1; suppose k1 + 1 = k2 ; ::_thesis: contradiction hence contradiction by A1, A5, A16, A32, A36, FINSEQ_4:67; ::_thesis: verum end; suppose k1 + 1 < k2 ; ::_thesis: contradiction then A38: k1 < ((len f) + 1) - 1 by A36, XREAL_1:20; then k1 in dom f by A12, A30, FINSEQ_1:1; then h /. k1 = f /. k1 by A5, FINSEQ_4:68; hence contradiction by A5, A13, A6, A30, A32, A36, A38, FINSEQ_4:67, TOPREAL3:39; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; supposeA39: ( k1 < (len f) + 1 & k2 < (len f) + 1 ) ; ::_thesis: contradiction then k2 <= len f by NAT_1:13; then A40: k2 in dom f by A12, A27, FINSEQ_1:1; k1 <= len f by A39, NAT_1:13; then A41: k1 in dom f by A12, A30, FINSEQ_1:1; then f . k1 = h . k1 by A5, FINSEQ_1:def_7 .= f . k2 by A5, A24, A29, A26, A40, FINSEQ_1:def_7 ; hence contradiction by A9, A25, A29, A26, A41, A40, FUNCT_1:def_4; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; hence h is one-to-one by FUNCT_1:def_4; :: according to TOPREAL1:def_8 ::_thesis: ( 2 <= len h & h is unfolded & h is s.n.c. & h is special ) 2 + 1 <= (len f) + 1 by A13, XREAL_1:6; hence len h >= 2 by A17, XXREAL_0:2; ::_thesis: ( h is unfolded & h is s.n.c. & h is special ) thus h is unfolded ::_thesis: ( h is s.n.c. & h is special ) proof let j be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= j or not j + 2 <= len h or (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} ) assume that A42: 1 <= j and A43: j + 2 <= len h ; ::_thesis: (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} A44: j + (1 + 1) = (j + 1) + 1 ; j + 1 <= j + 2 by XREAL_1:6; then A45: j + 1 <= len h by A43, XXREAL_0:2; now__::_thesis:_(LSeg_(h,j))_/\_(LSeg_(h,(j_+_1)))_=_{(h_/._(j_+_1))} percases ( j + 2 = len h or j + 2 < len h ) by A43, XXREAL_0:1; supposeA46: j + 2 = len h ; ::_thesis: (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} then A47: j + ((1 + 1) - 1) = len f by A17; then j <= len f by NAT_1:13; then j in dom f by A12, A42, FINSEQ_1:1; then A48: LSeg (h,j) = LSeg (f,j) by A5, A15, A47, TOPREAL3:18; j in NAT by ORDINAL1:def_12; then LSeg (h,j) in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A42, A47, A48; then A49: LSeg (h,j) = (LSeg (h,j)) /\ (L~ f) by XBOOLE_1:28, ZFMISC_1:74; h /. (j + 1) in LSeg (h,j) by A42, A45, TOPREAL1:21; then A50: {(h /. (j + 1))} c= LSeg (h,j) by ZFMISC_1:31; LSeg (h,(j + 1)) = LSeg ((f /. (len f)),p) by A17, A14, A18, A16, A46, TOPREAL1:def_3; hence (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = (LSeg (h,j)) /\ {(h /. (j + 1))} by A4, A17, A16, A46, A49, XBOOLE_1:16 .= {(h /. (j + 1))} by A50, XBOOLE_1:28 ; ::_thesis: verum end; suppose j + 2 < len h ; ::_thesis: (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} then A51: (j + (2 + 1)) - 1 <= len f by A17, NAT_1:13; then A52: (LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))} by A8, A42, A43, TOPREAL1:def_6; 1 <= j + 2 by A44, NAT_1:11; then A53: (j + 1) + 1 in dom f by A12, A51, FINSEQ_1:1; j + 1 <= j + 2 by A44, NAT_1:11; then A54: j + 1 <= len f by A51, XXREAL_0:2; 1 <= j + 1 by NAT_1:11; then A55: j + 1 in dom f by A12, A54, FINSEQ_1:1; then A56: h /. (j + 1) = f /. (j + 1) by A5, FINSEQ_4:68; j <= j + 1 by NAT_1:11; then j <= len f by A54, XXREAL_0:2; then j in dom f by A12, A42, FINSEQ_1:1; then LSeg (h,j) = LSeg (f,j) by A5, A55, TOPREAL3:18; hence (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} by A5, A52, A55, A53, A56, TOPREAL3:18; ::_thesis: verum end; end; end; hence (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} ; ::_thesis: verum end; thus h is s.n.c. ::_thesis: h is special proof let n, m be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( m <= n + 1 or LSeg (h,n) misses LSeg (h,m) ) assume A57: m > n + 1 ; ::_thesis: LSeg (h,n) misses LSeg (h,m) n <= n + 1 by NAT_1:11; then A58: n <= m by A57, XXREAL_0:2; A59: (n + 1) + 1 = n + (1 + 1) ; A60: 1 <= n + 1 by NAT_1:11; LSeg (f,n) misses LSeg (f,m) by A10, A57, TOPREAL1:def_7; then A61: (LSeg (f,n)) /\ (LSeg (f,m)) = {} by XBOOLE_0:def_7; now__::_thesis:_(LSeg_(h,n))_/\_(LSeg_(h,m))_=_{} percases ( m + 1 < len h or m + 1 = len h or m + 1 > len h ) by XXREAL_0:1; supposeA62: m + 1 < len h ; ::_thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {} then A63: m + 1 <= len f by A17, NAT_1:13; A64: 1 < m by A57, A60, XXREAL_0:2; then 1 <= m + 1 by NAT_1:13; then A65: m + 1 in dom f by A12, A63, FINSEQ_1:1; A66: m <= len f by A17, A62, XREAL_1:6; then m in dom f by A12, A64, FINSEQ_1:1; then A67: LSeg (h,m) = LSeg (f,m) by A5, A65, TOPREAL3:18; now__::_thesis:_(LSeg_(h,n))_/\_(LSeg_(h,m))_=_{} percases ( 0 < n or 0 = n ) ; suppose 0 < n ; ::_thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {} then A68: 0 + 1 <= n by NAT_1:13; n + 1 <= len f by A57, A66, XXREAL_0:2; then A69: n + 1 in dom f by A12, A60, FINSEQ_1:1; n <= len f by A58, A66, XXREAL_0:2; then n in dom f by A12, A68, FINSEQ_1:1; hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} by A5, A61, A67, A69, TOPREAL3:18; ::_thesis: verum end; suppose 0 = n ; ::_thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {} then LSeg (h,n) = {} by TOPREAL1:def_3; hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; ::_thesis: verum end; end; end; hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; ::_thesis: verum end; supposeA70: m + 1 = len h ; ::_thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {} now__::_thesis:_(LSeg_(h,n))_/\_(LSeg_(h,m))_=_{} percases ( 0 < n or 0 = n ) ; supposeA71: 0 < n ; ::_thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {} A72: n + 1 in dom f by A17, A12, A57, A60, A70, FINSEQ_1:1; A73: 0 + 1 <= n by A71, NAT_1:13; then n in dom f by A17, A12, A58, A70, FINSEQ_1:1; then A74: LSeg (h,n) = LSeg (f,n) by A5, A72, TOPREAL3:18; now__::_thesis:_not_(LSeg_(h,n))_/\_(LSeg_(h,m))_<>_{} set L = LSeg (f,n); set x = the Element of (LSeg (h,n)) /\ (LSeg (h,m)); assume A75: (LSeg (h,n)) /\ (LSeg (h,m)) <> {} ; ::_thesis: contradiction then A76: the Element of (LSeg (h,n)) /\ (LSeg (h,m)) in LSeg (f,n) by A74, XBOOLE_0:def_4; A77: the Element of (LSeg (h,n)) /\ (LSeg (h,m)) in LSeg ((f /. (len f)),p) by A17, A19, A70, A75, XBOOLE_0:def_4; n in NAT by ORDINAL1:def_12; then LSeg (f,n) in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A17, A57, A70, A73; then the Element of (LSeg (h,n)) /\ (LSeg (h,m)) in L~ f by A76, TARSKI:def_4; then the Element of (LSeg (h,n)) /\ (LSeg (h,m)) in {(f /. (len f))} by A4, A77, XBOOLE_0:def_4; then A78: the Element of (LSeg (h,n)) /\ (LSeg (h,m)) = f /. (len f) by TARSKI:def_1; A79: (n + 1) + 1 <= len f by A17, A57, A70, NAT_1:13; now__::_thesis:_contradiction percases ( (n + 1) + 1 = len f or (n + 1) + 1 < len f ) by A79, XXREAL_0:1; supposeA80: (n + 1) + 1 = len f ; ::_thesis: contradiction 1 <= n + 1 by NAT_1:11; then A81: f /. (len f) in LSeg (f,(n + 1)) by A80, TOPREAL1:21; (LSeg (f,n)) /\ (LSeg (f,(n + 1))) = {(f /. (n + 1))} by A8, A59, A73, A80, TOPREAL1:def_6; then f /. (len f) in {(f /. (n + 1))} by A76, A78, A81, XBOOLE_0:def_4; then f /. (len f) = f /. (n + 1) by TARSKI:def_1; then (len f) + 1 = len f by A15, A7, A72, A80, PARTFUN2:10; hence contradiction ; ::_thesis: verum end; supposeA82: (n + 1) + 1 < len f ; ::_thesis: contradiction reconsider j = (len f) - 1 as Element of NAT by A13, INT_1:5, XXREAL_0:2; (n + 2) + 1 <= len f by A82, NAT_1:13; then n + 2 <= (len f) - 1 by XREAL_1:19; then n + 1 < j by A59, NAT_1:13; then LSeg (f,n) misses LSeg (f,j) by A10, TOPREAL1:def_7; then A83: (LSeg (f,n)) /\ (LSeg (f,j)) = {} by XBOOLE_0:def_7; (1 + 1) - 1 = 1 ; then ( j + 1 = len f & 1 <= j ) by A13, XREAL_1:13; then f /. (len f) in LSeg (f,j) by TOPREAL1:21; hence contradiction by A76, A78, A83, XBOOLE_0:def_4; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; ::_thesis: verum end; suppose 0 = n ; ::_thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {} then LSeg (h,n) = {} by TOPREAL1:def_3; hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; ::_thesis: verum end; end; end; hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; ::_thesis: verum end; suppose m + 1 > len h ; ::_thesis: (LSeg (h,n)) /\ (LSeg (h,m)) = {} then LSeg (h,m) = {} by TOPREAL1:def_3; hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; ::_thesis: verum end; end; end; hence (LSeg (h,n)) /\ (LSeg (h,m)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum end; hereby :: according to TOPREAL1:def_5 ::_thesis: verum let n be Nat; ::_thesis: ( 1 <= n & n + 1 <= len h & not (h /. n) `1 = (h /. (n + 1)) `1 implies (h /. n) `2 = (h /. (n + 1)) `2 ) assume that A84: 1 <= n and A85: n + 1 <= len h ; ::_thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) set p3 = h /. n; set p4 = h /. (n + 1); now__::_thesis:_(_(h_/._n)_`1_=_(h_/._(n_+_1))_`1_or_(h_/._n)_`2_=_(h_/._(n_+_1))_`2_) percases ( n + 1 = len h or n + 1 < len h ) by A85, XXREAL_0:1; suppose n + 1 = len h ; ::_thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) by A1, A5, A17, A16, FINSEQ_4:67; ::_thesis: verum end; supposeA86: n + 1 < len h ; ::_thesis: ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) A87: 1 <= n + 1 by A84, NAT_1:13; n + 1 <= len f by A17, A86, NAT_1:13; then n + 1 in dom f by A12, A87, FINSEQ_1:1; then A88: h /. (n + 1) = f /. (n + 1) by A5, FINSEQ_4:68; n <= len f by A17, A86, XREAL_1:6; then n in dom f by A12, A84, FINSEQ_1:1; then A89: h /. n = f /. n by A5, FINSEQ_4:68; n + 1 <= len f by A17, A86, NAT_1:13; hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) by A20, A84, A89, A88, TOPREAL1:def_5; ::_thesis: verum end; end; end; hence ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 ) ; ::_thesis: verum end; end; 1 in dom f by A12, A14, FINSEQ_1:1; then h /. 1 = f /. 1 by A5, FINSEQ_4:68; hence L~ h is_S-P_arc_joining f /. 1,p by A18, A21, Def1; ::_thesis: L~ h c= (L~ f) \/ (Ball (u,r)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ h or x in (L~ f) \/ (Ball (u,r)) ) assume x in L~ h ; ::_thesis: x in (L~ f) \/ (Ball (u,r)) then consider X being set such that A90: x in X and A91: X in { (LSeg (h,m)) where m is Element of NAT : ( 1 <= m & m + 1 <= len h ) } by TARSKI:def_4; consider k being Element of NAT such that A92: X = LSeg (h,k) and A93: 1 <= k and A94: k + 1 <= len h by A91; percases ( k + 1 = len h or k + 1 < len h ) by A94, XXREAL_0:1; supposeA95: k + 1 = len h ; ::_thesis: x in (L~ f) \/ (Ball (u,r)) A96: Ball (u,r) c= (L~ f) \/ (Ball (u,r)) by XBOOLE_1:7; X c= Ball (u,r) by A2, A17, A19, A92, A95, TOPREAL3:21; hence x in (L~ f) \/ (Ball (u,r)) by A90, A96, TARSKI:def_3; ::_thesis: verum end; suppose k + 1 < len h ; ::_thesis: x in (L~ f) \/ (Ball (u,r)) then A97: k + 1 <= len f by A17, NAT_1:13; k <= k + 1 by NAT_1:11; then k <= len f by A97, XXREAL_0:2; then A98: k in dom f by A12, A93, FINSEQ_1:1; 1 <= k + 1 by A93, NAT_1:13; then k + 1 in dom f by A12, A97, FINSEQ_1:1; then X = LSeg (f,k) by A5, A92, A98, TOPREAL3:18; then X in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A93, A97; then x in union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A90, TARSKI:def_4; hence x in (L~ f) \/ (Ball (u,r)) by XBOOLE_0:def_3; ::_thesis: verum end; end; 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)) ) proof let p be Point of (TOP-REAL 2); ::_thesis: 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)) ) let f, h be FinSequence of (TOP-REAL 2); ::_thesis: 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)) ) let r be Real; ::_thesis: 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)) ) let u be Point of (Euclid 2); ::_thesis: ( 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))} implies ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) ) set p1 = f /. 1; set p2 = f /. (len f); assume that A1: f /. (len f) in Ball (u,r) and A2: p in Ball (u,r) and A3: |[(p `1),((f /. (len f)) `2)]| in Ball (u,r) and A4: f is being_S-Seq and A5: p `1 <> (f /. (len f)) `1 and A6: p `2 <> (f /. (len f)) `2 and A7: h = f ^ <*|[(p `1),((f /. (len f)) `2)]|,p*> and A8: ((LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) \/ (LSeg (|[(p `1),((f /. (len f)) `2)]|,p))) /\ (L~ f) = {(f /. (len f))} ; ::_thesis: ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) set p3 = |[(p `1),((f /. (len f)) `2)]|; set f1 = f ^ <*|[(p `1),((f /. (len f)) `2)]|*>; set h1 = (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ^ <*p*>; reconsider Lf = L~ f as non empty Subset of (TOP-REAL 2) by A8; A9: f /. (len f) in LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|) by RLTOPSP1:68; L~ f is_S-P_arc_joining f /. 1,f /. (len f) by A4, Def1; then Lf is_an_arc_of f /. 1,f /. (len f) by Th2; then f /. (len f) in L~ f by TOPREAL1:1; then f /. (len f) in (LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) /\ (L~ f) by A9, XBOOLE_0:def_4; then A10: ( (LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) /\ (L~ f) c= ((LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) /\ (L~ f)) \/ ((LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) /\ (L~ f)) & {(f /. (len f))} c= (LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) /\ (L~ f) ) by XBOOLE_1:7, ZFMISC_1:31; {(f /. (len f))} = ((LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) /\ (L~ f)) \/ ((LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) /\ (L~ f)) by A8, XBOOLE_1:23; then A11: (LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) /\ (L~ f) = {(f /. (len f))} by A10, XBOOLE_0:def_10; A12: len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) = (len f) + (len <*|[(p `1),((f /. (len f)) `2)]|*>) by FINSEQ_1:22 .= (len f) + 1 by FINSEQ_1:39 ; then A13: (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) /. (len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) = |[(p `1),((f /. (len f)) `2)]| by FINSEQ_4:67; A14: p = |[(p `1),(p `2)]| by EUCLID:53; A15: Seg (len f) = dom f by FINSEQ_1:def_3; len f >= 2 by A4, TOPREAL1:def_8; then A16: 1 <= len f by XXREAL_0:2; then len f in dom f by A15, FINSEQ_1:1; then A17: (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) /. (len f) = f /. (len f) by FINSEQ_4:68; A18: (LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) /\ (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) c= {|[(p `1),((f /. (len f)) `2)]|} proof set M1 = { (LSeg ((f ^ <*|[(p `1),((f /. (len f)) `2)]|*>),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ) } ; set Mf = { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ; assume not (LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) /\ (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) c= {|[(p `1),((f /. (len f)) `2)]|} ; ::_thesis: contradiction then consider x being set such that A19: x in (LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) /\ (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) and A20: not x in {|[(p `1),((f /. (len f)) `2)]|} by TARSKI:def_3; x in L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) by A19, XBOOLE_0:def_4; then consider X being set such that A21: x in X and A22: X in { (LSeg ((f ^ <*|[(p `1),((f /. (len f)) `2)]|*>),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ) } by TARSKI:def_4; consider k being Element of NAT such that A23: X = LSeg ((f ^ <*|[(p `1),((f /. (len f)) `2)]|*>),k) and A24: 1 <= k and A25: k + 1 <= len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) by A22; A26: x in LSeg (|[(p `1),((f /. (len f)) `2)]|,p) by A19, XBOOLE_0:def_4; now__::_thesis:_contradiction percases ( k + 1 = len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) or k + 1 < len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ) by A25, XXREAL_0:1; suppose k + 1 = len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ; ::_thesis: contradiction then LSeg ((f ^ <*|[(p `1),((f /. (len f)) `2)]|*>),k) = LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|) by A12, A13, A17, A24, TOPREAL1:def_3; then x in (LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) /\ (LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) by A26, A21, A23, XBOOLE_0:def_4; hence contradiction by A20, TOPREAL3:30; ::_thesis: verum end; suppose k + 1 < len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ; ::_thesis: contradiction then A27: k + 1 <= len f by A12, NAT_1:13; k <= k + 1 by NAT_1:11; then k <= len f by A27, XXREAL_0:2; then A28: k in dom f by A15, A24, FINSEQ_1:1; 1 <= k + 1 by A24, NAT_1:13; then k + 1 in dom f by A15, A27, FINSEQ_1:1; then X = LSeg (f,k) by A23, A28, TOPREAL3:18; then X in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A24, A27; then A29: x in L~ f by A21, TARSKI:def_4; x in (LSeg ((f /. (len f)),|[(p `1),((f /. (len f)) `2)]|)) \/ (LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) by A26, XBOOLE_0:def_3; then x in {(f /. (len f))} by A8, A29, XBOOLE_0:def_4; then x = f /. (len f) by TARSKI:def_1; hence contradiction by A5, A14, A26, TOPREAL3:11; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; A30: (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ^ <*p*> = f ^ (<*|[(p `1),((f /. (len f)) `2)]|*> ^ <*p*>) by FINSEQ_1:32 .= h by A7, FINSEQ_1:def_9 ; A31: ( |[(p `1),((f /. (len f)) `2)]| `2 = (f /. (len f)) `2 & |[(p `1),((f /. (len f)) `2)]| `1 = p `1 ) by EUCLID:52; then A32: f ^ <*|[(p `1),((f /. (len f)) `2)]|*> is being_S-Seq by A1, A3, A4, A5, A11, Th19; A33: L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) is_S-P_arc_joining f /. 1,|[(p `1),((f /. (len f)) `2)]| by A1, A3, A4, A5, A31, A11, Th19; then reconsider Lf1 = L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) as non empty Subset of (TOP-REAL 2) by Th1, TOPREAL1:26; A34: |[(p `1),((f /. (len f)) `2)]| in LSeg (|[(p `1),((f /. (len f)) `2)]|,p) by RLTOPSP1:68; A35: (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) /. (len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) = |[(p `1),((f /. (len f)) `2)]| by A12, FINSEQ_4:67; L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) c= (L~ f) \/ (Ball (u,r)) by A1, A3, A4, A5, A31, A11, Th19; then (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) \/ (Ball (u,r)) c= ((L~ f) \/ (Ball (u,r))) \/ (Ball (u,r)) by XBOOLE_1:9; then A36: (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) \/ (Ball (u,r)) c= (L~ f) \/ ((Ball (u,r)) \/ (Ball (u,r))) by XBOOLE_1:4; A37: ( ( p `1 = |[(p `1),((f /. (len f)) `2)]| `1 & p `2 <> |[(p `1),((f /. (len f)) `2)]| `2 ) or ( p `1 <> |[(p `1),((f /. (len f)) `2)]| `1 & p `2 = |[(p `1),((f /. (len f)) `2)]| `2 ) ) by A6, EUCLID:52; Lf1 is_an_arc_of f /. 1,|[(p `1),((f /. (len f)) `2)]| by A33, Th2; then |[(p `1),((f /. (len f)) `2)]| in L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) by TOPREAL1:1; then |[(p `1),((f /. (len f)) `2)]| in (LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) /\ (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) by A34, XBOOLE_0:def_4; then {|[(p `1),((f /. (len f)) `2)]|} c= (LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) /\ (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) by ZFMISC_1:31; then A38: (LSeg (|[(p `1),((f /. (len f)) `2)]|,p)) /\ (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) = {|[(p `1),((f /. (len f)) `2)]|} by A18, XBOOLE_0:def_10; 1 in dom f by A15, A16, FINSEQ_1:1; then (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) /. 1 = f /. 1 by FINSEQ_4:68; hence L~ h is_S-P_arc_joining f /. 1,p by A2, A3, A37, A32, A35, A38, A30, Th19; ::_thesis: L~ h c= (L~ f) \/ (Ball (u,r)) L~ ((f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ^ <*p*>) c= (L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)) \/ (Ball (u,r)) by A2, A3, A37, A32, A35, A38, Th19; hence L~ h c= (L~ f) \/ (Ball (u,r)) by A30, A36, XBOOLE_1:1; ::_thesis: verum 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)) ) proof let p be Point of (TOP-REAL 2); ::_thesis: 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)) ) let f, h be FinSequence of (TOP-REAL 2); ::_thesis: 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)) ) let r be Real; ::_thesis: 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)) ) let u be Point of (Euclid 2); ::_thesis: ( 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))} implies ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) ) set p1 = f /. 1; set p2 = f /. (len f); assume that A1: f /. (len f) in Ball (u,r) and A2: p in Ball (u,r) and A3: |[((f /. (len f)) `1),(p `2)]| in Ball (u,r) and A4: f is being_S-Seq and A5: p `1 <> (f /. (len f)) `1 and A6: p `2 <> (f /. (len f)) `2 and A7: h = f ^ <*|[((f /. (len f)) `1),(p `2)]|,p*> and A8: ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) \/ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p))) /\ (L~ f) = {(f /. (len f))} ; ::_thesis: ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) set p3 = |[((f /. (len f)) `1),(p `2)]|; set f1 = f ^ <*|[((f /. (len f)) `1),(p `2)]|*>; set h1 = (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) ^ <*p*>; reconsider Lf = L~ f as non empty Subset of (TOP-REAL 2) by A8; A9: f /. (len f) in LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|) by RLTOPSP1:68; L~ f is_S-P_arc_joining f /. 1,f /. (len f) by A4, Def1; then Lf is_an_arc_of f /. 1,f /. (len f) by Th2; then f /. (len f) in L~ f by TOPREAL1:1; then f /. (len f) in (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f) by A9, XBOOLE_0:def_4; then A10: ( (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f) c= ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f)) \/ ((LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ f)) & {(f /. (len f))} c= (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f) ) by XBOOLE_1:7, ZFMISC_1:31; {(f /. (len f))} = ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f)) \/ ((LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ f)) by A8, XBOOLE_1:23; then A11: (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f) = {(f /. (len f))} by A10, XBOOLE_0:def_10; A12: len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) = (len f) + (len <*|[((f /. (len f)) `1),(p `2)]|*>) by FINSEQ_1:22 .= (len f) + 1 by FINSEQ_1:39 ; then A13: (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) /. (len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) = |[((f /. (len f)) `1),(p `2)]| by FINSEQ_4:67; A14: p = |[(p `1),(p `2)]| by EUCLID:53; A15: Seg (len f) = dom f by FINSEQ_1:def_3; len f >= 2 by A4, TOPREAL1:def_8; then A16: 1 <= len f by XXREAL_0:2; then len f in dom f by A15, FINSEQ_1:1; then A17: (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) /. (len f) = f /. (len f) by FINSEQ_4:68; A18: (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) c= {|[((f /. (len f)) `1),(p `2)]|} proof set M1 = { (LSeg ((f ^ <*|[((f /. (len f)) `1),(p `2)]|*>),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) ) } ; set Mf = { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ; assume not (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) c= {|[((f /. (len f)) `1),(p `2)]|} ; ::_thesis: contradiction then consider x being set such that A19: x in (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) and A20: not x in {|[((f /. (len f)) `1),(p `2)]|} by TARSKI:def_3; x in L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) by A19, XBOOLE_0:def_4; then consider X being set such that A21: x in X and A22: X in { (LSeg ((f ^ <*|[((f /. (len f)) `1),(p `2)]|*>),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) ) } by TARSKI:def_4; consider k being Element of NAT such that A23: X = LSeg ((f ^ <*|[((f /. (len f)) `1),(p `2)]|*>),k) and A24: 1 <= k and A25: k + 1 <= len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) by A22; A26: x in LSeg (|[((f /. (len f)) `1),(p `2)]|,p) by A19, XBOOLE_0:def_4; now__::_thesis:_contradiction percases ( k + 1 = len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) or k + 1 < len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) ) by A25, XXREAL_0:1; suppose k + 1 = len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) ; ::_thesis: contradiction then LSeg ((f ^ <*|[((f /. (len f)) `1),(p `2)]|*>),k) = LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|) by A12, A13, A17, A24, TOPREAL1:def_3; then x in (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) by A26, A21, A23, XBOOLE_0:def_4; hence contradiction by A20, TOPREAL3:29; ::_thesis: verum end; suppose k + 1 < len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) ; ::_thesis: contradiction then A27: k + 1 <= len f by A12, NAT_1:13; k <= k + 1 by NAT_1:11; then k <= len f by A27, XXREAL_0:2; then A28: k in dom f by A15, A24, FINSEQ_1:1; 1 <= k + 1 by A24, NAT_1:13; then k + 1 in dom f by A15, A27, FINSEQ_1:1; then X = LSeg (f,k) by A23, A28, TOPREAL3:18; then X in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A24, A27; then A29: x in L~ f by A21, TARSKI:def_4; x in (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) \/ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) by A26, XBOOLE_0:def_3; then x in {(f /. (len f))} by A8, A29, XBOOLE_0:def_4; then x = f /. (len f) by TARSKI:def_1; hence contradiction by A6, A14, A26, TOPREAL3:12; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; A30: (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) ^ <*p*> = f ^ (<*|[((f /. (len f)) `1),(p `2)]|*> ^ <*p*>) by FINSEQ_1:32 .= h by A7, FINSEQ_1:def_9 ; A31: ( |[((f /. (len f)) `1),(p `2)]| `2 = p `2 & |[((f /. (len f)) `1),(p `2)]| `1 = (f /. (len f)) `1 ) by EUCLID:52; then A32: f ^ <*|[((f /. (len f)) `1),(p `2)]|*> is being_S-Seq by A1, A3, A4, A6, A11, Th19; A33: L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) is_S-P_arc_joining f /. 1,|[((f /. (len f)) `1),(p `2)]| by A1, A3, A4, A6, A31, A11, Th19; then reconsider Lf1 = L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) as non empty Subset of (TOP-REAL 2) by Th1, TOPREAL1:26; A34: |[((f /. (len f)) `1),(p `2)]| in LSeg (|[((f /. (len f)) `1),(p `2)]|,p) by RLTOPSP1:68; A35: (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) /. (len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) = |[((f /. (len f)) `1),(p `2)]| by A12, FINSEQ_4:67; L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) c= (L~ f) \/ (Ball (u,r)) by A1, A3, A4, A6, A31, A11, Th19; then (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) \/ (Ball (u,r)) c= ((L~ f) \/ (Ball (u,r))) \/ (Ball (u,r)) by XBOOLE_1:9; then A36: (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) \/ (Ball (u,r)) c= (L~ f) \/ ((Ball (u,r)) \/ (Ball (u,r))) by XBOOLE_1:4; A37: ( ( p `1 = |[((f /. (len f)) `1),(p `2)]| `1 & p `2 <> |[((f /. (len f)) `1),(p `2)]| `2 ) or ( p `1 <> |[((f /. (len f)) `1),(p `2)]| `1 & p `2 = |[((f /. (len f)) `1),(p `2)]| `2 ) ) by A5, EUCLID:52; Lf1 is_an_arc_of f /. 1,|[((f /. (len f)) `1),(p `2)]| by A33, Th2; then |[((f /. (len f)) `1),(p `2)]| in L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) by TOPREAL1:1; then |[((f /. (len f)) `1),(p `2)]| in (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) by A34, XBOOLE_0:def_4; then {|[((f /. (len f)) `1),(p `2)]|} c= (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) by ZFMISC_1:31; then A38: (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) = {|[((f /. (len f)) `1),(p `2)]|} by A18, XBOOLE_0:def_10; 1 in dom f by A15, A16, FINSEQ_1:1; then (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) /. 1 = f /. 1 by FINSEQ_4:68; hence L~ h is_S-P_arc_joining f /. 1,p by A2, A3, A37, A32, A35, A38, A30, Th19; ::_thesis: L~ h c= (L~ f) \/ (Ball (u,r)) L~ ((f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) ^ <*p*>) c= (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) \/ (Ball (u,r)) by A2, A3, A37, A32, A35, A38, Th19; hence L~ h c= (L~ f) \/ (Ball (u,r)) by A30, A36, XBOOLE_1:1; ::_thesis: verum 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)) ) proof let p be Point of (TOP-REAL 2); ::_thesis: 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)) ) let f be FinSequence of (TOP-REAL 2); ::_thesis: 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)) ) let r be Real; ::_thesis: 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)) ) let u be Point of (Euclid 2); ::_thesis: ( 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 implies 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)) ) ) set p1 = f /. 1; set Mf = { (LSeg (f,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } ; assume that A1: not f /. 1 in Ball (u,r) and A2: f /. (len f) in Ball (u,r) and A3: p in Ball (u,r) and A4: f is being_S-Seq and A5: not p in L~ f ; ::_thesis: 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)) ) A6: f is special by A4, TOPREAL1:def_8; defpred S1[ Nat] means ( 1 <= $1 & $1 <= (len f) - 1 & LSeg (f,$1) meets Ball (u,r) ); A7: len f >= 2 by A4, TOPREAL1:def_8; then reconsider n = (len f) - 1 as Element of NAT by INT_1:5, XXREAL_0:2; 2 = 1 + 1 ; then A8: 1 <= (len f) - 1 by A7, XREAL_1:19; n + 1 = len f ; then f /. (len f) in LSeg (f,n) by A8, TOPREAL1:21; then LSeg (f,n) meets Ball (u,r) by A2, XBOOLE_0:3; then A9: ex n being Nat st S1[n] by A8; consider m being Nat such that A10: S1[m] and A11: for i being Nat st S1[i] holds m <= i from NAT_1:sch_5(A9); reconsider m = m as Element of NAT by ORDINAL1:def_12; consider q1, q2 being Point of (TOP-REAL 2) such that A12: f /. m = q1 and A13: f /. (m + 1) = q2 ; A14: (LSeg (f,m)) /\ (Ball (u,r)) <> {} by A10, XBOOLE_0:def_7; A15: m + 1 <= len f by A10, XREAL_1:19; then A16: LSeg (f,m) = LSeg (q1,q2) by A10, A12, A13, TOPREAL1:def_3; m <= m + 1 by NAT_1:11; then A17: m <= len f by A15, XXREAL_0:2; A18: Seg (len f) = dom f by FINSEQ_1:def_3; A19: now__::_thesis:_not_(Ball_(u,r))_/\_(L~_(f_|_m))_<>_{} set x = the Element of (Ball (u,r)) /\ (L~ (f | m)); set M = { (LSeg ((f | m),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f | m) ) } ; A20: Seg (len (f | m)) = dom (f | m) by FINSEQ_1:def_3; assume A21: (Ball (u,r)) /\ (L~ (f | m)) <> {} ; ::_thesis: contradiction then A22: the Element of (Ball (u,r)) /\ (L~ (f | m)) in Ball (u,r) by XBOOLE_0:def_4; the Element of (Ball (u,r)) /\ (L~ (f | m)) in L~ (f | m) by A21, XBOOLE_0:def_4; then consider X being set such that A23: the Element of (Ball (u,r)) /\ (L~ (f | m)) in X and A24: X in { (LSeg ((f | m),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f | m) ) } by TARSKI:def_4; consider k being Element of NAT such that A25: X = LSeg ((f | m),k) and A26: 1 <= k and A27: k + 1 <= len (f | m) by A24; k <= k + 1 by NAT_1:11; then k <= len (f | m) by A27, XXREAL_0:2; then A28: k in Seg (len (f | m)) by A26, FINSEQ_1:1; 1 <= k + 1 by NAT_1:11; then k + 1 in Seg (len (f | m)) by A27, FINSEQ_1:1; then the Element of (Ball (u,r)) /\ (L~ (f | m)) in LSeg (f,k) by A23, A25, A28, A20, TOPREAL3:17; then A29: LSeg (f,k) meets Ball (u,r) by A22, XBOOLE_0:3; Seg m c= Seg (len f) by A17, FINSEQ_1:5; then A30: Seg m = (dom f) /\ (Seg m) by A18, XBOOLE_1:28 .= dom (f | (Seg m)) by RELAT_1:61 .= Seg (len (f | m)) by A20, FINSEQ_1:def_15 ; A31: (k + 1) - 1 <= (len (f | m)) - 1 by A27, XREAL_1:9; then A32: k <= m - 1 by A30, FINSEQ_1:6; m = len (f | m) by A30, FINSEQ_1:6; then (len (f | m)) - 1 <= (len f) - 1 by A17, XREAL_1:9; then k <= (len f) - 1 by A31, XXREAL_0:2; then m <= k by A11, A26, A29; then m <= m - 1 by A32, XXREAL_0:2; then 0 <= (m + (- 1)) - m by XREAL_1:48; hence contradiction ; ::_thesis: verum end; now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<=_(len_f)_-_1_&_(LSeg_(f,i))_/\_(Ball_(u,r))_<>_{}_holds_ m_<=_i let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= (len f) - 1 & (LSeg (f,i)) /\ (Ball (u,r)) <> {} implies m <= i ) assume that A33: ( 1 <= i & i <= (len f) - 1 ) and A34: (LSeg (f,i)) /\ (Ball (u,r)) <> {} ; ::_thesis: m <= i LSeg (f,i) meets Ball (u,r) by A34, XBOOLE_0:def_7; hence m <= i by A11, A33; ::_thesis: verum end; then A35: not q1 in Ball (u,r) by A1, A10, A12, TOPREAL3:26; set A = (LSeg (f,m)) /\ (Ball (u,r)); A36: ( q1 = |[(q1 `1),(q1 `2)]| & q2 = |[(q2 `1),(q2 `2)]| ) by EUCLID:53; m + 1 <= n + 1 by A10, XREAL_1:6; then LSeg (f,m) in { (LSeg (f,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } by A10; then A37: LSeg (f,m) c= union { (LSeg (f,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } by ZFMISC_1:74; now__::_thesis:_ex_g_being_FinSequence_of_the_carrier_of_(TOP-REAL_2)_st_ (_L~_g_is_S-P_arc_joining_f_/._1,p_&_L~_g_c=_(L~_f)_\/_(Ball_(u,r))_) percases ( ex q being Point of (TOP-REAL 2) st ( q in (LSeg (f,m)) /\ (Ball (u,r)) & ( p `1 = q `1 or p `2 = q `2 ) ) or for q being Point of (TOP-REAL 2) st q in (LSeg (f,m)) /\ (Ball (u,r)) holds ( p `1 <> q `1 & p `2 <> q `2 ) ) ; suppose ex q being Point of (TOP-REAL 2) st ( q in (LSeg (f,m)) /\ (Ball (u,r)) & ( p `1 = q `1 or p `2 = q `2 ) ) ; ::_thesis: ex g being FinSequence of the carrier of (TOP-REAL 2) st ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) ) then consider q being Point of (TOP-REAL 2) such that A38: q in (LSeg (f,m)) /\ (Ball (u,r)) and A39: ( p `1 = q `1 or p `2 = q `2 ) ; A40: q in Ball (u,r) by A38, XBOOLE_0:def_4; A41: q in LSeg (q,p) by RLTOPSP1:68; A42: q in LSeg (f,m) by A38, XBOOLE_0:def_4; then consider h being FinSequence of (TOP-REAL 2) such that A43: h is being_S-Seq and A44: h /. 1 = f /. 1 and A45: h /. (len h) = q and A46: L~ h is_S-P_arc_joining f /. 1,q and A47: L~ h c= L~ f and A48: L~ h = (L~ (f | m)) \/ (LSeg (q1,q)) by A1, A4, A12, A40, Th17; take g = h ^ <*p*>; ::_thesis: ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) ) A49: (L~ h) \/ (Ball (u,r)) c= (L~ f) \/ (Ball (u,r)) by A47, XBOOLE_1:9; A50: q in L~ f by A37, A42; A51: now__::_thesis:_(_(_p_`1_=_q_`1_&_p_`2_<>_q_`2_)_or_(_p_`1_<>_q_`1_&_p_`2_=_q_`2_)_) percases ( p `1 = q `1 or p `2 = q `2 ) by A39; suppose p `1 = q `1 ; ::_thesis: ( ( p `1 = q `1 & p `2 <> q `2 ) or ( p `1 <> q `1 & p `2 = q `2 ) ) hence ( ( p `1 = q `1 & p `2 <> q `2 ) or ( p `1 <> q `1 & p `2 = q `2 ) ) by A5, A50, TOPREAL3:6; ::_thesis: verum end; suppose p `2 = q `2 ; ::_thesis: ( ( p `1 = q `1 & p `2 <> q `2 ) or ( p `1 <> q `1 & p `2 = q `2 ) ) hence ( ( p `1 = q `1 & p `2 <> q `2 ) or ( p `1 <> q `1 & p `2 = q `2 ) ) by A5, A50, TOPREAL3:6; ::_thesis: verum end; end; end; A52: (LSeg (q,p)) /\ (L~ h) c= {q} proof A53: now__::_thesis:_(_q1_`1_=_q_`1_or_q1_`2_=_q_`2_) percases ( q1 `1 = q2 `1 or q1 `2 = q2 `2 ) by A6, A10, A15, A12, A13, TOPREAL1:def_5; suppose q1 `1 = q2 `1 ; ::_thesis: ( q1 `1 = q `1 or q1 `2 = q `2 ) hence ( q1 `1 = q `1 or q1 `2 = q `2 ) by A36, A16, A42, TOPREAL3:11; ::_thesis: verum end; suppose q1 `2 = q2 `2 ; ::_thesis: ( q1 `1 = q `1 or q1 `2 = q `2 ) hence ( q1 `1 = q `1 or q1 `2 = q `2 ) by A36, A16, A42, TOPREAL3:12; ::_thesis: verum end; end; end; LSeg (q,p) = (LSeg (q,p)) /\ (Ball (u,r)) by A3, A40, TOPREAL3:21, XBOOLE_1:28; then A54: (LSeg (q,p)) /\ ((L~ (f | m)) \/ (LSeg (q1,q))) = (((LSeg (q,p)) /\ (Ball (u,r))) /\ (L~ (f | m))) \/ ((LSeg (q,p)) /\ (LSeg (q1,q))) by XBOOLE_1:23 .= ((LSeg (q,p)) /\ ((Ball (u,r)) /\ (L~ (f | m)))) \/ ((LSeg (q,p)) /\ (LSeg (q1,q))) by XBOOLE_1:16 .= (LSeg (q1,q)) /\ (LSeg (q,p)) by A19 ; A55: now__::_thesis:_not_p_in_LSeg_(q1,q) q1 in LSeg (q1,q2) by RLTOPSP1:68; then A56: LSeg (q1,q) c= LSeg (f,m) by A16, A42, TOPREAL1:6; assume p in LSeg (q1,q) ; ::_thesis: contradiction hence contradiction by A5, A37, A56, TARSKI:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LSeg (q,p)) /\ (L~ h) or x in {q} ) assume x in (LSeg (q,p)) /\ (L~ h) ; ::_thesis: x in {q} hence x in {q} by A3, A35, A40, A51, A48, A54, A55, A53, TOPREAL3:42; ::_thesis: verum end; q in L~ h by A46, Th3; then q in (LSeg (q,p)) /\ (L~ h) by A41, XBOOLE_0:def_4; then {q} c= (LSeg (q,p)) /\ (L~ h) by ZFMISC_1:31; then A57: (LSeg (q,p)) /\ (L~ h) = {q} by A52, XBOOLE_0:def_10; then L~ g c= (L~ h) \/ (Ball (u,r)) by A3, A40, A51, A43, A45, Th19; hence ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) ) by A3, A40, A51, A43, A44, A45, A57, A49, Th19, XBOOLE_1:1; ::_thesis: verum end; supposeA58: for q being Point of (TOP-REAL 2) st q in (LSeg (f,m)) /\ (Ball (u,r)) holds ( p `1 <> q `1 & p `2 <> q `2 ) ; ::_thesis: 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)) ) set x = the Element of (LSeg (f,m)) /\ (Ball (u,r)); A59: the Element of (LSeg (f,m)) /\ (Ball (u,r)) in LSeg (f,m) by A14, XBOOLE_0:def_4; then reconsider q = the Element of (LSeg (f,m)) /\ (Ball (u,r)) as Point of (TOP-REAL 2) ; A60: ( q `1 <> p `1 & q `2 <> p `2 ) by A14, A58; q <> f /. 1 by A1, A14, XBOOLE_0:def_4; then consider h being FinSequence of (TOP-REAL 2) such that A61: h is being_S-Seq and A62: h /. 1 = f /. 1 and A63: h /. (len h) = q and A64: L~ h is_S-P_arc_joining f /. 1,q and A65: L~ h c= L~ f and A66: L~ h = (L~ (f | m)) \/ (LSeg (q1,q)) by A4, A12, A59, Th17; A67: q in Ball (u,r) by A14, XBOOLE_0:def_4; A68: ( q = |[(q `1),(q `2)]| & p = |[(p `1),(p `2)]| ) by EUCLID:53; now__::_thesis:_ex_g_being_FinSequence_of_the_carrier_of_(TOP-REAL_2)_st_ (_L~_g_is_S-P_arc_joining_f_/._1,p_&_L~_g_c=_(L~_f)_\/_(Ball_(u,r))_) percases ( |[(q `1),(p `2)]| in Ball (u,r) or |[(p `1),(q `2)]| in Ball (u,r) ) by A3, A67, A68, TOPREAL3:25; supposeA69: |[(q `1),(p `2)]| in Ball (u,r) ; ::_thesis: ex g being FinSequence of the carrier of (TOP-REAL 2) st ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) ) set v = |[(q `1),(p `2)]|; A70: ((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (L~ h) c= {q} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (L~ h) or x in {q} ) set L = (LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p)); assume A71: x in ((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (L~ h) ; ::_thesis: x in {q} ( LSeg (q,|[(q `1),(p `2)]|) c= Ball (u,r) & LSeg (|[(q `1),(p `2)]|,p) c= Ball (u,r) ) by A3, A67, A69, TOPREAL3:21; then (LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p)) = ((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (Ball (u,r)) by XBOOLE_1:8, XBOOLE_1:28; then A72: ((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ ((L~ (f | m)) \/ (LSeg (q1,q))) = ((((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (Ball (u,r))) /\ (L~ (f | m))) \/ (((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (LSeg (q1,q))) by XBOOLE_1:23 .= (((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ ((Ball (u,r)) /\ (L~ (f | m)))) \/ (((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (LSeg (q1,q))) by XBOOLE_1:16 .= {} \/ (((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (LSeg (q1,q))) by A19 ; A73: now__::_thesis:_(_q1_`1_=_q_`1_or_q1_`2_=_q_`2_) percases ( q1 `1 = q2 `1 or q1 `2 = q2 `2 ) by A6, A10, A15, A12, A13, TOPREAL1:def_5; suppose q1 `1 = q2 `1 ; ::_thesis: ( q1 `1 = q `1 or q1 `2 = q `2 ) hence ( q1 `1 = q `1 or q1 `2 = q `2 ) by A36, A16, A59, TOPREAL3:11; ::_thesis: verum end; suppose q1 `2 = q2 `2 ; ::_thesis: ( q1 `1 = q `1 or q1 `2 = q `2 ) hence ( q1 `1 = q `1 or q1 `2 = q `2 ) by A36, A16, A59, TOPREAL3:12; ::_thesis: verum end; end; end; now__::_thesis:_x_in_{q} percases ( q1 `1 = q `1 or q1 `2 = q `2 ) by A73; supposeA74: q1 `1 = q `1 ; ::_thesis: x in {q} now__::_thesis:_not_|[(q_`1),(p_`2)]|_in_LSeg_(q1,q) q1 in LSeg (q1,q2) by RLTOPSP1:68; then A75: LSeg (q1,q) c= LSeg (f,m) by A16, A59, TOPREAL1:6; A76: |[(q `1),(p `2)]| `2 = p `2 by EUCLID:52; assume |[(q `1),(p `2)]| in LSeg (q1,q) ; ::_thesis: contradiction then |[(q `1),(p `2)]| in (LSeg (f,m)) /\ (Ball (u,r)) by A69, A75, XBOOLE_0:def_4; hence contradiction by A58, A76; ::_thesis: verum end; hence x in {q} by A35, A67, A60, A66, A69, A72, A71, A74, TOPREAL3:43; ::_thesis: verum end; suppose q1 `2 = q `2 ; ::_thesis: x in {q} hence x in {q} by A14, A58, A66, A72, A71, TOPREAL3:27; ::_thesis: verum end; end; end; hence x in {q} ; ::_thesis: verum end; take g = h ^ <*|[(q `1),(p `2)]|,p*>; ::_thesis: ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) ) q in LSeg (q,|[(q `1),(p `2)]|) by RLTOPSP1:68; then A77: q in (LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p)) by XBOOLE_0:def_3; A78: (L~ h) \/ (Ball (u,r)) c= (L~ f) \/ (Ball (u,r)) by A65, XBOOLE_1:9; q in L~ h by A64, Th3; then q in ((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (L~ h) by A77, XBOOLE_0:def_4; then {q} c= ((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (L~ h) by ZFMISC_1:31; then A79: ((LSeg (q,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,p))) /\ (L~ h) = {q} by A70, XBOOLE_0:def_10; then L~ g c= (L~ h) \/ (Ball (u,r)) by A3, A67, A60, A61, A63, A69, Th21; hence ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) ) by A3, A67, A60, A61, A62, A63, A69, A79, A78, Th21, XBOOLE_1:1; ::_thesis: verum end; supposeA80: |[(p `1),(q `2)]| in Ball (u,r) ; ::_thesis: ex g being FinSequence of the carrier of (TOP-REAL 2) st ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) ) set v = |[(p `1),(q `2)]|; A81: ((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (L~ h) c= {q} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (L~ h) or x in {q} ) set L = (LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p)); assume A82: x in ((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (L~ h) ; ::_thesis: x in {q} ( LSeg (q,|[(p `1),(q `2)]|) c= Ball (u,r) & LSeg (|[(p `1),(q `2)]|,p) c= Ball (u,r) ) by A3, A67, A80, TOPREAL3:21; then (LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p)) = ((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (Ball (u,r)) by XBOOLE_1:8, XBOOLE_1:28; then A83: ((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ ((L~ (f | m)) \/ (LSeg (q1,q))) = ((((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (Ball (u,r))) /\ (L~ (f | m))) \/ (((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (LSeg (q1,q))) by XBOOLE_1:23 .= (((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ ((Ball (u,r)) /\ (L~ (f | m)))) \/ (((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (LSeg (q1,q))) by XBOOLE_1:16 .= {} \/ (((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (LSeg (q1,q))) by A19 ; A84: now__::_thesis:_(_q1_`1_=_q_`1_or_q1_`2_=_q_`2_) percases ( q1 `1 = q2 `1 or q1 `2 = q2 `2 ) by A6, A10, A15, A12, A13, TOPREAL1:def_5; suppose q1 `1 = q2 `1 ; ::_thesis: ( q1 `1 = q `1 or q1 `2 = q `2 ) hence ( q1 `1 = q `1 or q1 `2 = q `2 ) by A36, A16, A59, TOPREAL3:11; ::_thesis: verum end; suppose q1 `2 = q2 `2 ; ::_thesis: ( q1 `1 = q `1 or q1 `2 = q `2 ) hence ( q1 `1 = q `1 or q1 `2 = q `2 ) by A36, A16, A59, TOPREAL3:12; ::_thesis: verum end; end; end; now__::_thesis:_x_in_{q} percases ( q1 `1 = q `1 or q1 `2 = q `2 ) by A84; suppose q1 `1 = q `1 ; ::_thesis: x in {q} hence x in {q} by A14, A58, A66, A83, A82, TOPREAL3:28; ::_thesis: verum end; supposeA85: q1 `2 = q `2 ; ::_thesis: x in {q} now__::_thesis:_not_|[(p_`1),(q_`2)]|_in_LSeg_(q1,q) q1 in LSeg (q1,q2) by RLTOPSP1:68; then A86: LSeg (q1,q) c= LSeg (f,m) by A16, A59, TOPREAL1:6; A87: |[(p `1),(q `2)]| `1 = p `1 by EUCLID:52; assume |[(p `1),(q `2)]| in LSeg (q1,q) ; ::_thesis: contradiction then |[(p `1),(q `2)]| in (LSeg (f,m)) /\ (Ball (u,r)) by A80, A86, XBOOLE_0:def_4; hence contradiction by A58, A87; ::_thesis: verum end; hence x in {q} by A35, A67, A60, A66, A80, A83, A82, A85, TOPREAL3:44; ::_thesis: verum end; end; end; hence x in {q} ; ::_thesis: verum end; take g = h ^ <*|[(p `1),(q `2)]|,p*>; ::_thesis: ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) ) q in LSeg (q,|[(p `1),(q `2)]|) by RLTOPSP1:68; then A88: q in (LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p)) by XBOOLE_0:def_3; A89: (L~ h) \/ (Ball (u,r)) c= (L~ f) \/ (Ball (u,r)) by A65, XBOOLE_1:9; q in L~ h by A64, Th3; then q in ((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (L~ h) by A88, XBOOLE_0:def_4; then {q} c= ((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (L~ h) by ZFMISC_1:31; then A90: ((LSeg (q,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,p))) /\ (L~ h) = {q} by A81, XBOOLE_0:def_10; then L~ g c= (L~ h) \/ (Ball (u,r)) by A3, A67, A60, A61, A63, A80, Th20; hence ( L~ g is_S-P_arc_joining f /. 1,p & L~ g c= (L~ f) \/ (Ball (u,r)) ) by A3, A67, A60, A61, A62, A63, A80, A90, A89, Th20, XBOOLE_1:1; ::_thesis: verum end; end; end; hence 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)) ) ; ::_thesis: verum end; end; end; hence 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)) ) ; ::_thesis: verum 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 ) proof let R be Subset of (TOP-REAL 2); ::_thesis: 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 ) let p, p1, p2 be Point of (TOP-REAL 2); ::_thesis: 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 ) let P be Subset of (TOP-REAL 2); ::_thesis: 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 ) let r be Real; ::_thesis: 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 ) let u be Point of (Euclid 2); ::_thesis: ( 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 implies ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p1,p & P1 c= R ) ) assume that A1: p <> p1 and A2: P is_S-P_arc_joining p1,p2 and A3: P c= R and A4: p in Ball (u,r) and A5: p2 in Ball (u,r) and A6: Ball (u,r) c= R ; ::_thesis: ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p1,p & P1 c= R ) consider f being FinSequence of (TOP-REAL 2) such that A7: f is being_S-Seq and A8: P = L~ f and A9: p1 = f /. 1 and A10: p2 = f /. (len f) by A2, Def1; now__::_thesis:_ex_P1_being_Subset_of_(TOP-REAL_2)_st_ (_P1_is_S-P_arc_joining_p1,p_&_P1_c=_R_) percases ( p1 in Ball (u,r) or not p1 in Ball (u,r) ) ; suppose p1 in Ball (u,r) ; ::_thesis: ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p1,p & P1 c= R ) then consider P1 being Subset of (TOP-REAL 2) such that A11: ( P1 is_S-P_arc_joining p1,p & P1 c= Ball (u,r) ) by A1, A4, Th10; reconsider P1 = P1 as Subset of (TOP-REAL 2) ; take P1 = P1; ::_thesis: ( P1 is_S-P_arc_joining p1,p & P1 c= R ) thus ( P1 is_S-P_arc_joining p1,p & P1 c= R ) by A6, A11, XBOOLE_1:1; ::_thesis: verum end; supposeA12: not p1 in Ball (u,r) ; ::_thesis: ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p1,p & P1 c= R ) now__::_thesis:_ex_P1_being_Subset_of_(TOP-REAL_2)_st_ (_P1_is_S-P_arc_joining_p1,p_&_P1_c=_R_) percases ( p in P or not p in P ) ; suppose p in P ; ::_thesis: ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p1,p & P1 c= R ) then consider h being FinSequence of (TOP-REAL 2) such that h is being_S-Seq and h /. 1 = p1 and h /. (len h) = p and A13: ( L~ h is_S-P_arc_joining p1,p & L~ h c= L~ f ) by A1, A7, A8, A9, Th18; reconsider P1 = L~ h as Subset of (TOP-REAL 2) ; take P1 = P1; ::_thesis: ( P1 is_S-P_arc_joining p1,p & P1 c= R ) thus ( P1 is_S-P_arc_joining p1,p & P1 c= R ) by A3, A8, A13, XBOOLE_1:1; ::_thesis: verum end; suppose not p in P ; ::_thesis: ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p1,p & P1 c= R ) then consider h being FinSequence of (TOP-REAL 2) such that A14: L~ h is_S-P_arc_joining p1,p and A15: L~ h c= (L~ f) \/ (Ball (u,r)) by A4, A5, A7, A8, A9, A10, A12, Th22; reconsider P1 = L~ h as Subset of (TOP-REAL 2) ; take P1 = P1; ::_thesis: ( P1 is_S-P_arc_joining p1,p & P1 c= R ) thus P1 is_S-P_arc_joining p1,p by A14; ::_thesis: P1 c= R (L~ f) \/ (Ball (u,r)) c= R by A3, A6, A8, XBOOLE_1:8; hence P1 c= R by A15, XBOOLE_1:1; ::_thesis: verum end; end; end; hence ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p1,p & P1 c= R ) ; ::_thesis: verum end; end; end; hence ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p1,p & P1 c= R ) ; ::_thesis: verum 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 proof let R, P be Subset of (TOP-REAL 2); ::_thesis: 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 let p be Point of (TOP-REAL 2); ::_thesis: ( 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 ) ) ) } implies P is open ) assume that A1: R is being_Region and A2: 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 ) ) ) } ; ::_thesis: P is open reconsider RR = R, PP = P as Subset of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) ; R is open by A1, Def3; then A3: RR is open by PRE_TOPC:30; now__::_thesis:_for_u_being_Point_of_(Euclid_2)_st_u_in_P_holds_ ex_r_being_real_number_st_ (_r_>_0_&_Ball_(u,r)_c=_P_) let u be Point of (Euclid 2); ::_thesis: ( u in P implies ex r being real number st ( r > 0 & Ball (u,r) c= P ) ) reconsider p2 = u as Point of (TOP-REAL 2) by TOPREAL3:8; assume A4: u in P ; ::_thesis: ex r being real number st ( r > 0 & Ball (u,r) c= P ) then ex q1 being Point of (TOP-REAL 2) st ( q1 = u & q1 <> p & q1 in R & ( for P1 being Subset of (TOP-REAL 2) holds ( not P1 is_S-P_arc_joining p,q1 or not P1 c= R ) ) ) by A2; then consider r being real number such that A5: r > 0 and A6: Ball (u,r) c= RR by A3, Lm1, TOPMETR:15; take r = r; ::_thesis: ( r > 0 & Ball (u,r) c= P ) thus r > 0 by A5; ::_thesis: Ball (u,r) c= P reconsider r9 = r as Real by XREAL_0:def_1; A7: p2 in Ball (u,r9) by A5, TBSP_1:11; thus Ball (u,r) c= P ::_thesis: verum proof assume not Ball (u,r) c= P ; ::_thesis: contradiction then consider x being set such that A8: x in Ball (u,r) and A9: not x in P by TARSKI:def_3; x in R by A6, A8; then reconsider q = x as Point of (TOP-REAL 2) ; now__::_thesis:_contradiction percases ( q = p or ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q & P1 c= R ) ) by A2, A6, A8, A9; supposeA10: q = p ; ::_thesis: contradiction A11: now__::_thesis:_not_q_=_p2 assume A12: q = p2 ; ::_thesis: contradiction ex p3 being Point of (TOP-REAL 2) st ( p3 = p2 & p3 <> p & p3 in R & ( for P1 being Subset of (TOP-REAL 2) holds ( not P1 is_S-P_arc_joining p,p3 or not P1 c= R ) ) ) by A2, A4; hence contradiction by A10, A12; ::_thesis: verum end; u in Ball (u,r9) by A5, TBSP_1:11; then A13: ex P2 being Subset of (TOP-REAL 2) st ( P2 is_S-P_arc_joining q,p2 & P2 c= Ball (u,r9) ) by A8, A11, Th10; not p2 in P proof assume p2 in P ; ::_thesis: contradiction then ex q4 being Point of (TOP-REAL 2) st ( q4 = p2 & q4 <> p & q4 in R & ( for P1 being Subset of (TOP-REAL 2) holds ( not P1 is_S-P_arc_joining p,q4 or not P1 c= R ) ) ) by A2; hence contradiction by A6, A10, A13, XBOOLE_1:1; ::_thesis: verum end; hence contradiction by A4; ::_thesis: verum end; supposeA14: ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q & P1 c= R ) ; ::_thesis: contradiction not p2 in P proof assume p2 in P ; ::_thesis: contradiction then ex q4 being Point of (TOP-REAL 2) st ( q4 = p2 & q4 <> p & q4 in R & ( for P1 being Subset of (TOP-REAL 2) holds ( not P1 is_S-P_arc_joining p,q4 or not P1 c= R ) ) ) by A2; hence contradiction by A6, A7, A8, A14, Th23; ::_thesis: verum end; hence contradiction by A4; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; then PP is open by Lm1, TOPMETR:15; hence P is open by PRE_TOPC:30; ::_thesis: verum 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 proof let p be Point of (TOP-REAL 2); ::_thesis: 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 let R, P be Subset of (TOP-REAL 2); ::_thesis: ( 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 ) ) } implies P is open ) assume that A1: R is being_Region and A2: p in R and A3: 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 ) ) } ; ::_thesis: P is open reconsider RR = R, PP = P as Subset of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) ; R is open by A1, Def3; then A4: RR is open by PRE_TOPC:30; now__::_thesis:_for_u_being_Point_of_(Euclid_2)_st_u_in_P_holds_ ex_r_being_real_number_st_ (_r_>_0_&_Ball_(u,r)_c=_P_) let u be Point of (Euclid 2); ::_thesis: ( u in P implies ex r being real number st ( r > 0 & Ball (u,r) c= P ) ) reconsider p2 = u as Point of (TOP-REAL 2) by TOPREAL3:8; assume u in P ; ::_thesis: ex r being real number st ( r > 0 & Ball (u,r) c= P ) then consider q1 being Point of (TOP-REAL 2) such that A5: q1 = u and A6: ( q1 = p or ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q1 & P1 c= R ) ) by A3; now__::_thesis:_p2_in_R percases ( q1 = p or ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q1 & P1 c= R ) ) by A6; suppose q1 = p ; ::_thesis: p2 in R hence p2 in R by A2, A5; ::_thesis: verum end; suppose ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q1 & P1 c= R ) ; ::_thesis: p2 in R then consider P2 being Subset of (TOP-REAL 2) such that A7: P2 is_S-P_arc_joining p,q1 and A8: P2 c= R ; p2 in P2 by A5, A7, Th3; hence p2 in R by A8; ::_thesis: verum end; end; end; then consider r being real number such that A9: r > 0 and A10: Ball (u,r) c= RR by A4, Lm1, TOPMETR:15; take r = r; ::_thesis: ( r > 0 & Ball (u,r) c= P ) thus r > 0 by A9; ::_thesis: Ball (u,r) c= P reconsider r9 = r as Real by XREAL_0:def_1; A11: p2 in Ball (u,r9) by A9, TBSP_1:11; thus Ball (u,r) c= P ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ball (u,r) or x in P ) assume A12: x in Ball (u,r) ; ::_thesis: x in P then reconsider q = x as Point of (TOP-REAL 2) by A10, TARSKI:def_3; now__::_thesis:_x_in_P percases ( q = p or q <> p ) ; suppose q = p ; ::_thesis: x in P hence x in P by A3; ::_thesis: verum end; supposeA13: q <> p ; ::_thesis: x in P A14: now__::_thesis:_(_q1_=_p_implies_x_in_P_) assume q1 = p ; ::_thesis: x in P then p in Ball (u,r9) by A5, A9, TBSP_1:11; then consider P2 being Subset of (TOP-REAL 2) such that A15: P2 is_S-P_arc_joining p,q and A16: P2 c= Ball (u,r9) by A12, A13, Th10; reconsider P2 = P2 as Subset of (TOP-REAL 2) ; P2 c= R by A10, A16, XBOOLE_1:1; hence x in P by A3, A15; ::_thesis: verum end; now__::_thesis:_(_q1_<>_p_implies_x_in_P_) assume q1 <> p ; ::_thesis: x in P then ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q & P1 c= R ) by A5, A6, A10, A11, A12, A13, Th23; hence x in P by A3; ::_thesis: verum end; hence x in P by A14; ::_thesis: verum end; end; end; hence x in P ; ::_thesis: verum end; end; then PP is open by Lm1, TOPMETR:15; hence P is open by PRE_TOPC:30; ::_thesis: verum 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 proof let p be Point of (TOP-REAL 2); ::_thesis: 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 let R, P be Subset of (TOP-REAL 2); ::_thesis: ( 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 ) ) } implies P c= R ) assume that A1: p in R and A2: 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 ) ) } ; ::_thesis: P c= R let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in R ) assume x in P ; ::_thesis: x in R then consider q being Point of (TOP-REAL 2) such that A3: q = x and A4: ( q = p or ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q & P1 c= R ) ) by A2; now__::_thesis:_x_in_R percases ( q = p or ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q & P1 c= R ) ) by A4; suppose q = p ; ::_thesis: x in R hence x in R by A1, A3; ::_thesis: verum end; suppose ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q & P1 c= R ) ; ::_thesis: x in R then consider P1 being Subset of (TOP-REAL 2) such that A5: P1 is_S-P_arc_joining p,q and A6: P1 c= R ; q in P1 by A5, Th3; hence x in R by A3, A6; ::_thesis: verum end; end; end; hence x in R ; ::_thesis: verum 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 proof let p be Point of (TOP-REAL 2); ::_thesis: 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 let R, P be Subset of (TOP-REAL 2); ::_thesis: ( 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 ) ) } implies R c= P ) assume that A1: R is being_Region and A2: p in R and A3: 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 ) ) } ; ::_thesis: R c= P A4: p in P by A3; set P2 = R \ P; reconsider P22 = R \ P as Subset of (TOP-REAL 2) ; A5: [#] ((TOP-REAL 2) | R) = R by PRE_TOPC:def_5; then reconsider P11 = P, P12 = P22 as Subset of ((TOP-REAL 2) | R) by A2, A3, Th26, XBOOLE_1:36; P \/ (R \ P) = P \/ R by XBOOLE_1:39; then A6: [#] ((TOP-REAL 2) | R) = P11 \/ P12 by A5, XBOOLE_1:12; now__::_thesis:_for_x_being_set_holds_ (_x_in_R_\_P_iff_x_in__{__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_)_)_)__}__) let x be set ; ::_thesis: ( x in R \ P iff x in { 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 ) ) ) } ) A7: now__::_thesis:_(_x_in_R_\_P_implies_x_in__{__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_)_)_)__}__) assume A8: x in R \ P ; ::_thesis: x in { 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 ) ) ) } then reconsider q2 = x as Point of (TOP-REAL 2) ; not x in P by A8, XBOOLE_0:def_5; then A9: ( q2 <> p & ( for P1 being Subset of (TOP-REAL 2) holds ( not P1 is_S-P_arc_joining p,q2 or not P1 c= R ) ) ) by A3; q2 in R by A8, XBOOLE_0:def_5; hence x in { 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 ) ) ) } by A9; ::_thesis: verum end; now__::_thesis:_(_x_in__{__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_)_)_)__}__implies_x_in_R_\_P_) assume x in { 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 ) ) ) } ; ::_thesis: x in R \ P then A10: ex q3 being Point of (TOP-REAL 2) st ( q3 = x & q3 <> p & q3 in R & ( for P1 being Subset of (TOP-REAL 2) holds ( not P1 is_S-P_arc_joining p,q3 or not P1 c= R ) ) ) ; then for q being Point of (TOP-REAL 2) holds ( not q = x or ( not q = p & ( for P1 being Subset of (TOP-REAL 2) holds ( not P1 is_S-P_arc_joining p,q or not P1 c= R ) ) ) ) ; then not x in P by A3; hence x in R \ P by A10, XBOOLE_0:def_5; ::_thesis: verum end; hence ( x in R \ P iff x in { 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 ) ) ) } ) by A7; ::_thesis: verum end; then R \ 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 ) ) ) } by TARSKI:1; then P22 is open by A1, Th24; then A11: P22 in the topology of (TOP-REAL 2) by PRE_TOPC:def_2; reconsider R9 = R as non empty Subset of (TOP-REAL 2) by A2; R is connected by A1, Def3; then A12: (TOP-REAL 2) | R9 is connected by CONNSP_1:def_3; P is open by A1, A2, A3, Th25; then A13: P in the topology of (TOP-REAL 2) by PRE_TOPC:def_2; P11 = P /\ ([#] ((TOP-REAL 2) | R)) by XBOOLE_1:28; then P11 in the topology of ((TOP-REAL 2) | R) by A13, PRE_TOPC:def_4; then A14: P11 is open by PRE_TOPC:def_2; P12 = P22 /\ ([#] ((TOP-REAL 2) | R)) by XBOOLE_1:28; then P12 in the topology of ((TOP-REAL 2) | R) by A11, PRE_TOPC:def_4; then A15: P12 is open by PRE_TOPC:def_2; A16: P11 misses P12 by XBOOLE_1:79; then P11 /\ P12 = {} ((TOP-REAL 2) | R) by XBOOLE_0:def_7; then R \ P = {} by A4, A12, A16, A6, A14, A15, CONNSP_1:11; hence R c= P by XBOOLE_1:37; ::_thesis: verum 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 proof let p be Point of (TOP-REAL 2); ::_thesis: 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 let R, P be Subset of (TOP-REAL 2); ::_thesis: ( 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 ) ) } implies R = P ) assume A1: ( 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 ) ) } ) ; ::_thesis: R = P hence R c= P by Th27; :: according to XBOOLE_0:def_10 ::_thesis: P c= R thus P c= R by A1, Th26; ::_thesis: verum 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 ) proof let p, q be Point of (TOP-REAL 2); ::_thesis: 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 ) let R be Subset of (TOP-REAL 2); ::_thesis: ( R is being_Region & p in R & q in R & p <> q implies ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= R ) ) set RR = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 = p or ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) } ; { q2 where q2 is Point of (TOP-REAL 2) : ( q2 = p or ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 = p or ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) } or x in the carrier of (TOP-REAL 2) ) assume x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 = p or ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex q2 being Point of (TOP-REAL 2) st ( q2 = x & ( q2 = p or ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; then reconsider RR = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 = p or ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) } as Subset of (TOP-REAL 2) ; assume that A1: ( R is being_Region & p in R ) and A2: q in R and A3: p <> q ; ::_thesis: ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= R ) R c= RR by A1, Th27; then q in RR by A2; then ex q1 being Point of (TOP-REAL 2) st ( q1 = q & ( q1 = p or ex P1 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p,q1 & P1 c= R ) ) ) ; hence ex P being Subset of (TOP-REAL 2) st ( P is_S-P_arc_joining p,q & P c= R ) by A3; ::_thesis: verum end;