:: 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;