:: Behaviour of an Arc Crossing a Line
:: by Yatsuka Nakamura
::
:: Received January 26, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, EUCLID, PRE_TOPC, TOPREAL1, JORDAN6, JORDAN3,
TARSKI, REAL_1, RLTOPSP1, MCART_1, XXREAL_0, ARYTM_1, RELAT_1, ARYTM_3,
CARD_1, SUPINF_2, SPPOL_2, FINSEQ_1, PARTFUN1, XBOOLE_0, FUNCT_1,
TOPMETR, BORSUK_1, TOPS_2, ORDINAL2, XXREAL_1, SEQ_4, STRUCT_0, XXREAL_2,
METRIC_1, COMPLEX1, RCOMP_1, PCOMPS_1, RELAT_2, BORSUK_2, GRAPH_1,
TOPREAL4, NAT_1, JORDAN20, FUNCT_2;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, XCMPLX_0, XXREAL_0,
XXREAL_2, XREAL_0, COMPLEX1, REAL_1, ORDINAL1, NAT_1, NAT_D, PARTFUN1,
FUNCT_2, SEQ_4, FINSEQ_1, STRUCT_0, CONNSP_1, RCOMP_1, METRIC_1,
PCOMPS_1, JORDAN5C, JORDAN6, RLVECT_1, RLTOPSP1, EUCLID, TOPMETR,
PRE_TOPC, TOPS_2, NUMBERS, PSCOMP_1, BORSUK_2, TOPREAL4, TOPREAL1,
SPPOL_2, FINSEQ_6;
constructors REAL_1, SQUARE_1, RCOMP_1, CONNSP_1, TOPS_2, TOPREAL1, TOPREAL4,
PSCOMP_1, BORSUK_2, JORDAN5C, JORDAN6, BINOP_2, NAT_D, SEQ_4, CONVEX1,
FINSEQ_6, PCOMPS_1;
registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, NAT_1,
MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, EUCLID, TOPMETR,
XXREAL_2, RLTOPSP1, RELAT_1, ORDINAL1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
equalities STRUCT_0, RLTOPSP1;
expansions TARSKI;
theorems TARSKI, TOPREAL1, XBOOLE_0, JORDAN6, TOPS_2, XBOOLE_1, SEQ_4,
RELAT_1, PSCOMP_1, FUNCT_2, TOPREAL3, JORDAN5C, TOPREAL5, RCOMP_1,
TOPMETR, ABSVALUE, METRIC_1, JORDAN16, XREAL_0, FUNCT_1, PRE_TOPC,
BORSUK_1, BORSUK_4, FRECHET, PCOMPS_1, NAT_1, XCMPLX_1, JORDAN2B,
UNIFORM1, GOBOARD6, TREAL_1, BORSUK_2, CONNSP_1, TOPMETR3, JORDAN5B,
GOBOARD7, JGRAPH_2, TOPREAL4, FINSEQ_4, FINSEQ_1, SPRECT_4, SPRECT_3,
FINSEQ_3, XREAL_1, COMPLEX1, XXREAL_0, PARTFUN1, XXREAL_1, XXREAL_2,
NAT_D, RLTOPSP1, FINSEQ_6, RLVECT_1;
schemes NAT_1;
begin
theorem Th1:
for P being Subset of TOP-REAL 2, p1,p2,p being Point of TOP-REAL
2 st P is_an_arc_of p1,p2 & p in P holds Segment(P,p1,p2,p,p)={p}
proof
let P be Subset of TOP-REAL 2,p1,p2,p be Point of TOP-REAL 2;
assume that
A1: P is_an_arc_of p1,p2 and
A2: p in P;
A3: Segment(P,p1,p2,p,p)={q where q is Point of TOP-REAL 2: LE p,q,P,p1,p2 &
LE q,p,P,p1,p2} by JORDAN6:26;
A4: {p} c= Segment(P,p1,p2,p,p)
proof
let x be object;
assume x in {p};
then
A5: x=p by TARSKI:def 1;
LE p,p,P,p1,p2 by A2,JORDAN5C:9;
hence thesis by A3,A5;
end;
Segment(P,p1,p2,p,p)c= {p}
proof
let x be object;
assume x in Segment(P,p1,p2,p,p);
then consider q being Point of TOP-REAL 2 such that
A6: x=q and
A7: LE p,q,P,p1,p2 & LE q,p,P,p1,p2 by A3;
p=q by A1,A7,JORDAN5C:12;
hence thesis by A6,TARSKI:def 1;
end;
hence thesis by A4,XBOOLE_0:def 10;
end;
theorem Th2:
for p1,p2,p being Point of TOP-REAL 2,a being Real st p in LSeg(
p1,p2) & p1`1<=a & p2`1<=a holds p`1<=a
proof
let p1,p2,p be Point of TOP-REAL 2,a be Real;
assume that
A1: p in LSeg(p1,p2) and
A2: p1`1<=a and
A3: p2`1<=a;
consider r being Real such that
A4: p = (1-r)*p1+r*p2 and
A5: 0<=r and
A6: r<=1 by A1;
A7: p`1 = ((1-r)*p1)`1+(r*p2)`1 by A4,TOPREAL3:2
.= ((1-r)*p1)`1+r*p2`1 by TOPREAL3:4
.= (1-r)*p1`1+r*p2`1 by TOPREAL3:4;
1-r>=0 by A6,XREAL_1:48;
then
A8: (1-r)*p1`1<=(1-r)*a by A2,XREAL_1:64;
A9: (1-r)*a+r*a= a;
r*p2`1<=r*a by A3,A5,XREAL_1:64;
hence thesis by A7,A8,A9,XREAL_1:7;
end;
theorem Th3:
for p1,p2,p being Point of TOP-REAL 2,a being Real st p in LSeg(
p1,p2) & p1`1>=a & p2`1>=a holds p`1>=a
proof
let p1,p2,p be Point of TOP-REAL 2,a be Real;
assume that
A1: p in LSeg(p1,p2) and
A2: p1`1>=a and
A3: p2`1>=a;
consider r being Real such that
A4: p = (1-r)*p1+r*p2 and
A5: 0<=r and
A6: r<=1 by A1;
A7: p`1 = ((1-r)*p1)`1+(r*p2)`1 by A4,TOPREAL3:2
.= ((1-r)*p1)`1+r*p2`1 by TOPREAL3:4
.= (1-r)*p1`1+r*p2`1 by TOPREAL3:4;
1-r>=0 by A6,XREAL_1:48;
then
A8: (1-r)*p1`1>=(1-r)*a by A2,XREAL_1:64;
A9: (1-r)*a+r*a= a;
r*p2`1>=r*a by A3,A5,XREAL_1:64;
hence thesis by A7,A8,A9,XREAL_1:7;
end;
theorem
for p1,p2,p being Point of TOP-REAL 2,a being Real st p in LSeg(p1,p2)
& p1`1<a & p2`1<a holds p`1<a
proof
let p1,p2,p be Point of TOP-REAL 2,a be Real;
assume that
A1: p in LSeg(p1,p2) and
A2: p1`1<a and
A3: p2`1<a;
consider r being Real such that
A4: p = (1-r)*p1+r*p2 and
A5: 0<=r and
A6: r<=1 by A1;
A7: p`1 = ((1-r)*p1)`1+(r*p2)`1 by A4,TOPREAL3:2
.= ((1-r)*p1)`1+r*p2`1 by TOPREAL3:4
.= (1-r)*p1`1+r*p2`1 by TOPREAL3:4;
per cases;
suppose
0=r;
then p=p1+(0)*p2 by A4,RLVECT_1:def 8
.=p1+0.TOP-REAL 2 by RLVECT_1:10
.=p1 by RLVECT_1:4;
hence thesis by A2;
end;
suppose
A8: 0<>r;
A9: (1-r)*a+r*a= a;
1-r>=0 by A6,XREAL_1:48;
then
A10: (1-r)*p1`1<=(1-r)*a by A2,XREAL_1:64;
r*p2`1<r*a by A3,A5,A8,XREAL_1:68;
hence thesis by A7,A10,A9,XREAL_1:8;
end;
end;
theorem
for p1,p2,p being Point of TOP-REAL 2,a being Real st p in LSeg(p1,p2)
& p1`1>a & p2`1>a holds p`1>a
proof
let p1,p2,p be Point of TOP-REAL 2,a be Real;
assume that
A1: p in LSeg(p1,p2) and
A2: p1`1>a and
A3: p2`1>a;
consider r being Real such that
A4: p = (1-r)*p1+r*p2 and
A5: 0<=r and
A6: r<=1 by A1;
A7: p`1 = ((1-r)*p1)`1+(r*p2)`1 by A4,TOPREAL3:2
.= ((1-r)*p1)`1+r*p2`1 by TOPREAL3:4
.= (1-r)*p1`1+r*p2`1 by TOPREAL3:4;
per cases;
suppose
0=r;
then p=p1+(0)*p2 by A4,RLVECT_1:def 8
.=p1+0.TOP-REAL 2 by RLVECT_1:10
.=p1 by RLVECT_1:4;
hence thesis by A2;
end;
suppose
A8: 0<>r;
A9: (1-r)*a+r*a= a;
1-r>=0 by A6,XREAL_1:48;
then
A10: (1-r)*p1`1>=(1-r)*a by A2,XREAL_1:64;
r*p2`1>r*a by A3,A5,A8,XREAL_1:68;
hence thesis by A7,A10,A9,XREAL_1:8;
end;
end;
reserve j for Nat;
theorem Th6:
for f being S-Sequence_in_R2, p,q being Point of TOP-REAL 2 st 1
<=j & j < len f & p in LSeg(f,j) & q in LSeg(f,j) & (f/.j)`2=(f/.(j+1))`2 & (f
/.j)`1>(f/.(j+1))`1 & LE p,q,L~f,f/.1,f/.(len f) holds p`1>=q`1
proof
let f be S-Sequence_in_R2, p,q be Point of TOP-REAL 2;
assume that
A1: 1 <=j and
A2: j < len f and
A3: p in LSeg(f,j) and
A4: q in LSeg(f,j) and
A5: (f/.j)`2=(f/.(j+1))`2 and
A6: (f/.j)`1>(f/.(j+1))`1 and
A7: LE p,q,L~f,f/.1,f/.(len f);
j+1<=len f by A2,NAT_1:13;
then
A8: LSeg(f,j)=LSeg(f/.j,f/.(j+1)) by A1,TOPREAL1:def 3;
per cases;
suppose
A9: p`1<> (f/.j)`1;
(f/.j)`1>=p`1 by A3,A6,A8,TOPREAL1:3;
then (f/.j)`1>p`1 by A9,XXREAL_0:1;
then
A10: (f/.j)`1-p`1>0 by XREAL_1:50;
now
reconsider a=((f/.j)`1-q`1)/((f/.j)`1-p`1) as Real;
A11: (1-a)=((f/.j)`1-p`1)/((f/.j)`1-p`1)- ((f/.j)`1-q`1)/((f/.j)`1-p`1)
by A10,XCMPLX_1:60
.=((f/.j)`1-p`1- ((f/.j)`1-q`1))/((f/.j)`1-p`1) by XCMPLX_1:120
.=(q`1-p`1)/((f/.j)`1-p`1);
A12: ((1-a)*(f/.j)+a*p)`1=((1-a)*(f/.j))`1+(a*p)`1 by TOPREAL3:2
.=(1-a)*(f/.j)`1+ (a*p)`1 by TOPREAL3:4
.=1* (f/.j)`1 -a*(f/.j)`1 +a*(p`1) by TOPREAL3:4
.= (f/.j)`1 -(a*((f/.j)`1 -(p`1)))
.= (f/.j)`1 -((f/.j)`1-q`1) by A10,XCMPLX_1:87
.=q`1;
(f/.j)`1>=q`1 by A4,A6,A8,TOPREAL1:3;
then
A13: (f/.j)`1-q`1>=0 by XREAL_1:48;
A14: p`2=(f/.j)`2 by A3,A5,A8,GOBOARD7:6;
((1-a)*(f/.j)+a*p)`2=((1-a)*(f/.j))`2+(a*p)`2 by TOPREAL3:2
.=(1-a)*(f/.j)`2+ (a*p)`2 by TOPREAL3:4
.=1* (f/.j)`2 -a*(f/.j)`2 +a*(p`2) by TOPREAL3:4
.=q`2 by A4,A5,A8,A14,GOBOARD7:6;
then
A15: q=(1-a)*(f/.j)+a*p by A12,TOPREAL3:6;
assume
A16: p`1<q`1;
then q`1-p`1>0 by XREAL_1:50;
then 1-a+a>=0+a by A10,A11,XREAL_1:7;
then q in LSeg(f/.j,p) by A10,A13,A15;
then LE q,p,L~f,f/.1,f/.(len f) by A1,A2,A3,SPRECT_3:23;
hence contradiction by A7,A16,JORDAN5C:12,TOPREAL1:25;
end;
hence thesis;
end;
suppose
p`1=(f/.j)`1;
hence thesis by A4,A6,A8,TOPREAL1:3;
end;
end;
theorem Th7:
for f being S-Sequence_in_R2, p,q being Point of TOP-REAL 2 st 1
<=j & j < len f & p in LSeg(f,j) & q in LSeg(f,j) & (f/.j)`2=(f/.(j+1))`2 & (f
/.j)`1<(f/.(j+1))`1 & LE p,q,L~f,f/.1,f/.(len f) holds p`1<=q`1
proof
let f be S-Sequence_in_R2, p,q be Point of TOP-REAL 2;
assume that
A1: 1 <=j and
A2: j < len f and
A3: p in LSeg(f,j) and
A4: q in LSeg(f,j) and
A5: (f/.j)`2=(f/.(j+1))`2 and
A6: (f/.j)`1<(f/.(j+1))`1 and
A7: LE p,q,L~f,f/.1,f/.(len f);
j+1<=len f by A2,NAT_1:13;
then
A8: LSeg(f,j)=LSeg(f/.j,f/.(j+1)) by A1,TOPREAL1:def 3;
per cases;
suppose
A9: p`1<> (f/.(j))`1;
(f/.j)`1<=p`1 by A3,A6,A8,TOPREAL1:3;
then (f/.(j))`1<p`1 by A9,XXREAL_0:1;
then
A10: (f/.(j))`1 -p`1<0 by XREAL_1:49;
now
reconsider a=((f/.(j))`1-q`1)/((f/.(j))`1-p`1) as Real;
A11: (1-a)=((f/.(j))`1-p`1)/((f/.(j))`1-p`1) - ((f/.(j))`1-q`1)/((f/.(j)
)`1-p`1) by A10,XCMPLX_1:60
.=((f/.(j))`1-p`1- ((f/.(j))`1-q`1))/((f/.(j))`1-p`1) by XCMPLX_1:120
.=(q`1-p`1)/((f/.(j))`1-p`1);
A12: ((1-a)*(f/.(j))+a*p)`1=((1-a)*(f/.(j)))`1+(a*p)`1 by TOPREAL3:2
.=(1-a)*(f/.(j))`1+ (a*p)`1 by TOPREAL3:4
.=1* (f/.(j))`1 -a*(f/.(j))`1 +a*(p`1) by TOPREAL3:4
.= (f/.(j))`1 -(a*((f/.(j))`1 -(p`1)))
.= (f/.(j))`1 -((f/.(j))`1-q`1) by A10,XCMPLX_1:87
.=q`1;
(f/.j)`1<=q`1 by A4,A6,A8,TOPREAL1:3;
then
A13: (f/.(j))`1-q`1<=0 by XREAL_1:47;
A14: p`2=(f/.j)`2 by A3,A5,A8,GOBOARD7:6;
((1-a)*(f/.(j))+a*p)`2=((1-a)*(f/.(j)))`2+(a*p)`2 by TOPREAL3:2
.=(1-a)*(f/.(j))`2+ (a*p)`2 by TOPREAL3:4
.=1* (f/.(j))`2 -a*(f/.(j))`2 +a*(p`2) by TOPREAL3:4
.=q`2 by A4,A5,A8,A14,GOBOARD7:6;
then
A15: q=(1-a)*(f/.(j))+a*p by A12,TOPREAL3:6;
assume
A16: p`1>q`1;
then q`1-p`1<0 by XREAL_1:49;
then 1-a+a>=0+a by A10,A11,XREAL_1:7;
then q in LSeg(f/.(j),p) by A10,A13,A15;
then LE q,p,L~f,f/.1,f/.(len f) by A1,A2,A3,SPRECT_3:23;
hence contradiction by A7,A16,JORDAN5C:12,TOPREAL1:25;
end;
hence thesis;
end;
suppose
p`1=(f/.(j))`1;
hence thesis by A4,A6,A8,TOPREAL1:3;
end;
end;
definition
let P be Subset of TOP-REAL 2,
p1,p2,p be Point of TOP-REAL 2, e be Real;
pred p is_Lin P,p1,p2,e means
P is_an_arc_of p1,p2 & p in P & p`1=e &
ex p4 being Point of TOP-REAL 2 st p4`1<e & LE p4,p,P,p1,p2 & for p5 being
Point of TOP-REAL 2 st LE p4,p5,P,p1,p2 & LE p5,p,P,p1,p2 holds p5`1<=e;
pred p is_Rin P,p1,p2,e means
P is_an_arc_of p1,p2 & p in P & p`1=e &
ex p4 being Point of TOP-REAL 2 st p4`1>e & LE p4,p,P,p1,p2 & for p5 being
Point of TOP-REAL 2 st LE p4,p5,P,p1,p2 & LE p5,p,P,p1,p2 holds p5`1>=e;
pred p is_Lout P,p1,p2,e means
P is_an_arc_of p1,p2 & p in P & p`1=e
& ex p4 being Point of TOP-REAL 2 st p4`1<e & LE p,p4,P,p1,p2 & for p5 being
Point of TOP-REAL 2 st LE p5,p4,P,p1,p2 & LE p,p5,P,p1,p2 holds p5`1<=e;
pred p is_Rout P,p1,p2,e means
P is_an_arc_of p1,p2 & p in P & p`1=e
& ex p4 being Point of TOP-REAL 2 st p4`1>e & LE p,p4,P,p1,p2 & for p5 being
Point of TOP-REAL 2 st LE p5,p4,P,p1,p2 & LE p,p5,P,p1,p2 holds p5`1>=e;
pred p is_OSin P,p1,p2,e means
P is_an_arc_of p1,p2 & p in P & p`1=e
& ex p7 being Point of TOP-REAL 2 st LE p7,p,P,p1,p2 & (for p8 being Point of
TOP-REAL 2 st LE p7,p8,P,p1,p2 & LE p8,p,P,p1,p2 holds p8`1=e) & for p4 being
Point of TOP-REAL 2 st LE p4,p7,P,p1,p2 & p4<>p7 holds (ex p5 being Point of
TOP-REAL 2 st LE p4,p5,P,p1,p2 & LE p5,p7,P,p1,p2 & p5`1>e) & ex p6 being Point
of TOP-REAL 2 st LE p4,p6,P,p1,p2 & LE p6,p7,P,p1,p2 & p6`1<e;
pred p is_OSout P,p1,p2,e means
P is_an_arc_of p1,p2 & p in P & p`1=e
& ex p7 being Point of TOP-REAL 2 st LE p,p7,P,p1,p2 & (for p8 being Point of
TOP-REAL 2 st LE p8,p7,P,p1,p2 & LE p,p8,P,p1,p2 holds p8`1=e) & for p4 being
Point of TOP-REAL 2 st LE p7,p4,P,p1,p2 & p4<>p7 holds (ex p5 being Point of
TOP-REAL 2 st LE p5,p4,P,p1,p2 & LE p7,p5,P,p1,p2 & p5`1>e)& ex p6 being Point
of TOP-REAL 2 st LE p6,p4,P,p1,p2 & LE p7,p6,P,p1,p2 & p6`1<e;
correctness;
end;
theorem
for P being Subset of TOP-REAL 2, p1,p2,p being Point of TOP-REAL 2,e
being Real st P is_an_arc_of p1,p2 & p1`1<=e & p2`1>=e holds ex p3 being Point
of TOP-REAL 2 st p3 in P & p3`1=e
proof
let P be Subset of TOP-REAL 2, p1,p2,p be Point of TOP-REAL 2,e be Real;
set x = the Element of P /\ Vertical_Line(e);
assume P is_an_arc_of p1,p2 & p1`1<=e & p2`1>=e;
then P meets Vertical_Line(e) by JORDAN6:49;
then
A1: P /\ Vertical_Line(e) <> {} by XBOOLE_0:def 7;
then x in Vertical_Line(e) by XBOOLE_0:def 4;
then x in {p3 where p3 is Point of TOP-REAL 2: p3`1=e} by JORDAN6:def 6;
then
A2: ex p4 being Point of TOP-REAL 2 st p4=x & p4`1=e;
x in P by A1,XBOOLE_0:def 4;
hence thesis by A2;
end;
theorem
for P being non empty Subset of TOP-REAL 2, p1,p2,p being Point of
TOP-REAL 2,e being Real st P is_an_arc_of p1,p2 & p1`1<e & p in P & p`1=e holds
p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e or p is_OSin P,p1,p2,e
proof
let P be non empty Subset of TOP-REAL 2, p1,p2,p be Point of TOP-REAL 2,e be
Real;
assume that
A1: P is_an_arc_of p1,p2 and
A2: p1`1<e and
A3: p in P and
A4: p`1=e;
now
reconsider pr1a=proj1 as Function of TOP-REAL 2,R^1 by TOPMETR:17;
reconsider pro1=pr1a|P as Function of (TOP-REAL 2)|P,R^1 by PRE_TOPC:9;
consider f being Function of I[01], (TOP-REAL 2)|P such that
A5: f is being_homeomorphism and
A6: f.0 = p1 and
A7: f.1 = p2 by A1,TOPREAL1:def 1;
A8: f is continuous by A5,TOPS_2:def 5;
A9: rng f=[#]((TOP-REAL 2)|P) by A5,TOPS_2:def 5;
then p in rng f by A3,PRE_TOPC:def 5;
then consider xs being object such that
A10: xs in dom f and
A11: p=f.xs by FUNCT_1:def 3;
A12: dom f=[#](I[01]) by A5,TOPS_2:def 5;
then reconsider s2=xs as Element of REAL by A10,BORSUK_1:40;
A13: 0<=s2 by A10,BORSUK_1:40,XXREAL_1:1;
A14: 0 in REAL by XREAL_0:def 1;
for q being Point of TOP-REAL 2 st q=f.0 holds q`1<>e by A2,A6;
then
A15: 0 in {s where s is Element of REAL: 0<=s & s<=s2 &
(for q being Point of
TOP-REAL 2 st q=f.s holds q`1<>e)} by A13,A14;
{s where s is Element of REAL: 0<=s & s<=s2 &
for q being Point of TOP-REAL 2 st
q=f.s holds q`1<>e } c= REAL
proof
let x be object;
assume x in
{s where s is Element of REAL: 0<=s & s<=s2 & (for q being Point of
TOP-REAL 2 st q=f.s holds q`1<>e)};
then ex s being Element of REAL
st s=x & 0<=s & s<=s2 & for q being Point of
TOP-REAL 2 st q=f.s holds q`1<>e;
hence thesis;
end;
then reconsider R={s where s is Element of REAL: 0<=s & s<=s2 &
(for q being Point of
TOP-REAL 2 st q=f.s holds q`1<>e)} as non empty Subset of REAL by A15;
A16: s2<=1 by A10,BORSUK_1:40,XXREAL_1:1;
R c= [.0,1.]
proof
let x be object;
assume x in R;
then consider s being Element of REAL such that
A17: s=x & 0<=s and
A18: s<=s2 and
for q being Point of TOP-REAL 2 st q=f.s holds q`1<>e;
s<=1 by A16,A18,XXREAL_0:2;
hence thesis by A17,XXREAL_1:1;
end;
then reconsider R99=R as Subset of I[01] by BORSUK_1:40;
reconsider s0=upper_bound R as Element of REAL by XREAL_0:def 1;
A19: for s being Real st s in R holds s < s2
proof
let s be Real;
assume s in R;
then
A20: ex s3 being Element of REAL
st s3=s & 0<=s3 & s3<=s2 & for q being Point of
TOP-REAL 2 st q=f.s3 holds q`1<>e;
then s<>s2 by A4,A11;
hence thesis by A20,XXREAL_0:1;
end;
then for s being Real st s in R holds s <= s2;
then
A21: s0 <= s2 by SEQ_4:45;
then
A22: s0 <=1 by A16,XXREAL_0:2;
R99=R;
then
A23: 0 <= s0 by A15,BORSUK_4:26;
then s0 in dom f by A12,A22,BORSUK_1:40,XXREAL_1:1;
then f.s0 in rng f by FUNCT_1:def 3;
then f.s0 in P by A9,PRE_TOPC:def 5;
then reconsider p9=f.s0 as Point of TOP-REAL 2;
A24: LE p9,p,P,p1,p2 by A1,A5,A6,A7,A11,A16,A23,A21,A22,JORDAN5C:8;
for p7 being Point of (TOP-REAL 2)|P holds pro1.p7=proj1.p7
proof
let p7 be Point of (TOP-REAL 2)|P;
the carrier of ((TOP-REAL 2)|P)=P by PRE_TOPC:8;
hence thesis by FUNCT_1:49;
end;
then
A25: pro1 is continuous by JGRAPH_2:29;
reconsider h=pro1*f as Function of I[01],R^1;
A26: dom h=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
for s being ExtReal st s in R holds s <= s2 by A19;
then s2 is UpperBound of R by XXREAL_2:def 1;
then
A27: R is bounded_above by XXREAL_2:def 10;
A28: rng f=P by A9,PRE_TOPC:def 5;
A29: for p8 being Point of TOP-REAL 2 st LE p9,p8,P,p1,p2 & LE p8,p,P,p1,
p2 holds p8`1=e
proof
let p8 be Point of TOP-REAL 2;
assume that
A30: LE p9,p8,P,p1,p2 and
A31: LE p8,p,P,p1,p2;
A32: p8 in P by A30,JORDAN5C:def 3;
then consider x8 being object such that
A33: x8 in dom f and
A34: p8=f.x8 by A28,FUNCT_1:def 3;
reconsider s8=x8 as Element of REAL by A12,A33,BORSUK_1:40;
A35: s8<=1 by A33,BORSUK_1:40,XXREAL_1:1;
then
A36: s8<=s2 by A5,A6,A7,A11,A13,A16,A31,A34,JORDAN5C:def 3;
A37: 0<=s8 by A33,BORSUK_1:40,XXREAL_1:1;
then
A38: s0 <=s8 by A5,A6,A7,A22,A30,A34,A35,JORDAN5C:def 3;
now
reconsider s8n=s8 as Point of RealSpace by METRIC_1:def 13;
reconsider s8m=s8 as Point of Closed-Interval-MSpace(0,1) by A33,
BORSUK_1:40,TOPMETR:10;
reconsider ee=|.p8`1-e.|/2 as Real;
reconsider w=p8`1 as Element of RealSpace
by METRIC_1:def 13,XREAL_0:def 1;
reconsider B=Ball(w,ee) as Subset of R^1 by METRIC_1:def 13,TOPMETR:17;
A39: B={s7 where s7 is Real:p8`1-ee<s7 & s7<p8`1+ee} by JORDAN2B:17
.= ].p8`1-ee,p8`1+ee.[ by RCOMP_1:def 2;
assume
A40: p8`1<>e;
then p8`1-e<>0;
then |.p8`1-e.|>0 by COMPLEX1:47;
then
A41: w in Ball(w,ee) by GOBOARD6:1,XREAL_1:139;
A42: h"B is open & I[01]=TopSpaceMetr(Closed-Interval-MSpace(0,1)) by A8,A25
,TOPMETR:20,def 6,def 7,UNIFORM1:2;
h.s8=pro1.(f.s8) by A26,A33,BORSUK_1:40,FUNCT_1:12
.=proj1.p8 by A32,A34,FUNCT_1:49
.=p8`1 by PSCOMP_1:def 5;
then s8 in h"B by A26,A33,A41,BORSUK_1:40,FUNCT_1:def 7;
then consider r0 being Real such that
A43: r0>0 and
A44: Ball(s8m,r0) c= h"B by A42,TOPMETR:15;
reconsider r0 as Real;
reconsider r01=min(s2-s8,r0) as Real;
s8<s2 by A4,A11,A34,A36,A40,XXREAL_0:1;
then s2-s8>0 by XREAL_1:50;
then
A45: r01>0 by A43,XXREAL_0:21;
then
A46: r01-r01/2+r01/2>0+r01/2 by XREAL_1:6;
then
A47: s8+r01/2<s8+r01 by XREAL_1:6;
reconsider s70=s8+r01/2 as Real;
the carrier of Closed-Interval-MSpace(0,1)=[.0,1.] & Ball(s8n,r01
)= (].s8- r01,s8+r01 .[) by FRECHET:7,TOPMETR:10;
then
A48: Ball(s8m,r01)= (].s8-r01,s8+r01 .[) /\ [.0,1.] by TOPMETR:9;
s2-s8>=r01 by XXREAL_0:17;
then
A49: s2-s8+s8>=r01+s8 by XREAL_1:7;
then
A50: s70<=s2 by A47,XXREAL_0:2;
s8+r01<=1 by A16,A49,XXREAL_0:2;
then s8+r01/2<1 by A47,XXREAL_0:2;
then
A51: s8+r01/2 in [.0,1.] by A37,A45,XXREAL_1:1;
Ball(s8m,r01) c= Ball(s8m,r0) by PCOMPS_1:1,XXREAL_0:17;
then
A52: (].s8-r01,s8+r01 .[)/\ [.0,1.] c= h"B by A44,A48;
s8+0<s8+(r01/2+r01) by A45,XREAL_1:6;
then s8-r01+r01<s8+r01/2+r01;
then
A53: s8-r01<s8+r01/2 by XREAL_1:6;
s8+r01/2<s8+r01 by A46,XREAL_1:6;
then s8+r01/2 in ].s8-r01,s8+r01 .[ by A53,XXREAL_1:4;
then
A54: s8+r01/2 in (].s8-r01,s8+r01 .[)/\ [.0,1.] by A51,XBOOLE_0:def 4;
then
A55: h.(s8+r01/2) in B by A52,FUNCT_1:def 7;
A56: s8+r01/2 in dom h by A52,A54,FUNCT_1:def 7;
A57: for p7 being Point of TOP-REAL 2 st p7=f.s70 holds p7`1<>e
proof
let p7 be Point of TOP-REAL 2;
assume
A58: p7=f.s70;
s70<=1 by A16,A50,XXREAL_0:2;
then s70 in [.0,1.] by A37,A45,XXREAL_1:1;
then
A59: p7 in rng f by A12,A58,BORSUK_1:40,FUNCT_1:def 3;
A60: rng f=[#]((TOP-REAL 2)|P) by A5,TOPS_2:def 5
.=P by PRE_TOPC:def 5;
A61: h.s70=pro1.(f.s70) by A56,FUNCT_1:12
.=pr1a.(p7) by A58,A59,A60,FUNCT_1:49
.=p7`1 by PSCOMP_1:def 5;
then
A62: p7`1<p8`1+ee by A39,A55,XXREAL_1:4;
A63: p8`1-ee<p7`1 by A39,A55,A61,XXREAL_1:4;
now
assume
A64: p7`1=e;
now
per cases;
case
A65: p8`1-e>=0;
then p8`1-(p8`1-e)/2<e by A63,A64,ABSVALUE:def 1;
then p8`1/2+e/2<e/2+e/2;
then p8`1/2<e/2 by XREAL_1:7;
then
A66: p8`1/2-e/2<e/2-e/2 by XREAL_1:14;
(p8`1-e)/2>=0/2 by A65;
hence contradiction by A66;
end;
case
A67: p8`1-e<0;
then e< p8`1+(-(p8`1-e))/2 by A62,A64,ABSVALUE:def 1;
then p8`1/2+e/2>e/2+e/2;
then p8`1/2>e/2 by XREAL_1:7;
then
A68: p8`1/2-e/2>e/2-e/2 by XREAL_1:14;
(p8`1-e)/2<=0/2 by A67;
hence contradiction by A68;
end;
end;
hence contradiction;
end;
hence thesis;
end;
s8<s70 by A45,XREAL_1:29,139;
then consider s7 being Real such that
A69: s8<s7 and
A70: 0<=s7 & s7<=s2 & for p7 being Point of TOP-REAL 2 st p7=f.s7
holds p7`1 <>e by A37,A50,A57;
reconsider s7 as Element of REAL by XREAL_0:def 1;
s7 in R by A70;
then s7 <= s0 by A27,SEQ_4:def 1;
hence contradiction by A38,A69,XXREAL_0:2;
end;
hence thesis;
end;
assume not p is_OSin P,p1,p2,e;
then consider p4 being Point of TOP-REAL 2 such that
A71: LE p4,p9,P,p1,p2 and
A72: p4<>p9 and
A73: (for p5 being Point of TOP-REAL 2 st LE p4,p5,P,p1,p2 & LE p5,p9
, P,p1,p2 holds p5`1<=e)or for p6 being Point of TOP-REAL 2 st LE p4,p6,P,p1,p2
& LE p6,p9,P,p1,p2 holds p6`1>=e by A1,A3,A4,A24,A29;
A74: p9 in P by A71,JORDAN5C:def 3;
now
per cases by A73;
case
A75: for p5 being Point of TOP-REAL 2 st LE p4,p5,P,p1,p2 & LE p5
,p9,P,p1,p2 holds p5`1<=e;
A76: now
p4 in P by A71,JORDAN5C:def 3;
then p4 in rng f by A9,PRE_TOPC:def 5;
then consider xs4 being object such that
A77: xs4 in dom f and
A78: p4=f.xs4 by FUNCT_1:def 3;
reconsider s4=xs4 as Real by A77;
A79: 0<=s4 by A77,BORSUK_1:40,XXREAL_1:1;
A80: s4<=1 by A77,BORSUK_1:40,XXREAL_1:1;
assume
A81: not ex p51 being Point of TOP-REAL 2 st LE p4,p51,P,p1,p2
& LE p51,p9,P,p1,p2 & p51`1<e;
A82: for p51 being Point of TOP-REAL 2 st LE p4,p51,P,p1,p2 & LE
p51,p9,P,p1,p2 holds p51`1=e
proof
let p51 be Point of TOP-REAL 2;
assume LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2;
then p51`1>=e & p51`1<=e by A75,A81;
hence thesis by XXREAL_0:1;
end;
A83: now
assume s4< s0;
then
A84: s0-s4>0 by XREAL_1:50;
then
A85: s4<s4+(s0-s4)/2 by XREAL_1:29,139;
(s0-s4)/2>0 by A84,XREAL_1:139;
then consider r being Real such that
A86: r in R and
A87: s0-((s0-s4)/2)<r by A27,SEQ_4:def 1;
reconsider rss=r as Real;
A88: ex s7 being Element of REAL
st s7=r & 0<=s7 & s7<=s2 & for q being Point
of TOP-REAL 2 st q=f.s7 holds q`1<>e by A86;
then
A89: r<=1 by A16,XXREAL_0:2;
then r in [.0,1.] by A79,A85,A87,XXREAL_1:1;
then f.rss in rng f by A12,BORSUK_1:40,FUNCT_1:def 3;
then f.rss in P by A9,PRE_TOPC:def 5;
then reconsider pss=f.rss as Point of TOP-REAL 2;
s4<r by A85,A87,XXREAL_0:2;
then
A90: LE p4,pss,P,p1,p2 by A1,A5,A6,A7,A78,A79,A80,A89,JORDAN5C:8;
r<=s0 by A27,A86,SEQ_4:def 1;
then LE pss,p9,P,p1,p2 by A1,A5,A6,A7,A22,A79,A85,A87,A89,
JORDAN5C:8;
then pss`1=e by A82,A90;
hence contradiction by A88;
end;
s4<= s0 by A5,A6,A7,A23,A22,A71,A78,A80,JORDAN5C:def 3;
hence contradiction by A72,A78,A83,XXREAL_0:1;
end;
now
assume ex p51 being Point of TOP-REAL 2 st LE p4,p51,P,p1,p2 & LE
p51,p9,P,p1,p2 & p51`1<e;
then consider p51 being Point of TOP-REAL 2 such that
A91: LE p4,p51,P,p1,p2 and
A92: LE p51,p9,P,p1,p2 and
A93: p51`1<e;
A94: for p5 being Point of TOP-REAL 2 st LE p51,p5,P,p1,p2 & LE p5,
p,P,p1,p2 holds p5`1<=e
proof
let p5 be Point of TOP-REAL 2;
assume that
A95: LE p51,p5,P,p1,p2 and
A96: LE p5,p,P,p1,p2;
A97: LE p4,p5,P,p1,p2 by A91,A95,JORDAN5C:13;
A98: p5 in P by A95,JORDAN5C:def 3;
then
A99: p5=p9 implies LE p9,p5,P,p1,p2 by JORDAN5C:9;
now
per cases by A1,A74,A98,A99,JORDAN5C:14;
case
LE p5,p9,P,p1,p2;
hence thesis by A75,A97;
end;
case
LE p9,p5,P,p1,p2;
hence thesis by A29,A96;
end;
end;
hence thesis;
end;
LE p51,p,P,p1,p2 by A24,A92,JORDAN5C:13;
hence p is_Lin P,p1,p2,e by A1,A3,A4,A93,A94;
end;
hence p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e by A76;
end;
case
A100: for p6 being Point of TOP-REAL 2 st LE p4,p6,P,p1,p2 & LE p6
,p9,P,p1,p2 holds p6`1>=e;
A101: now
p4 in P by A71,JORDAN5C:def 3;
then p4 in rng f by A9,PRE_TOPC:def 5;
then consider xs4 being object such that
A102: xs4 in dom f and
A103: p4=f.xs4 by FUNCT_1:def 3;
reconsider s4=xs4 as Real by A102;
A104: 0<=s4 by A102,BORSUK_1:40,XXREAL_1:1;
A105: s4<=1 by A102,BORSUK_1:40,XXREAL_1:1;
assume
A106: not ex p51 being Point of TOP-REAL 2 st LE p4,p51,P,p1,p2
& LE p51,p9,P,p1,p2 & p51`1>e;
A107: for p51 being Point of TOP-REAL 2 st LE p4,p51,P,p1,p2 & LE
p51,p9,P,p1,p2 holds p51`1=e
proof
let p51 be Point of TOP-REAL 2;
assume LE p4,p51,P,p1,p2 & LE p51,p9,P,p1,p2;
then p51`1<=e & p51`1>=e by A100,A106;
hence thesis by XXREAL_0:1;
end;
A108: now
assume s4<s0;
then
A109: s0-s4>0 by XREAL_1:50;
then
A110: s4<s4+(s0-s4)/2 by XREAL_1:29,139;
(s0-s4)/2>0 by A109,XREAL_1:139;
then consider r being Real such that
A111: r in R and
A112: s0-((s0-s4)/2)<r by A27,SEQ_4:def 1;
reconsider rss=r as Real;
A113: ex s7 being Element of REAL
st s7=r & 0<=s7 & s7<=s2 & for q being Point
of TOP-REAL 2 st q=f.s7 holds q`1<>e by A111;
then
A114: r<=1 by A16,XXREAL_0:2;
then r in [.0,1.] by A104,A110,A112,XXREAL_1:1;
then f.rss in rng f by A12,BORSUK_1:40,FUNCT_1:def 3;
then f.rss in P by A9,PRE_TOPC:def 5;
then reconsider pss=f.rss as Point of TOP-REAL 2;
s4<r by A110,A112,XXREAL_0:2;
then
A115: LE p4,pss,P,p1,p2 by A1,A5,A6,A7,A103,A104,A105,A114,JORDAN5C:8;
r<=s0 by A27,A111,SEQ_4:def 1;
then LE pss,p9,P,p1,p2 by A1,A5,A6,A7,A22,A104,A110,A112,A114,
JORDAN5C:8;
then pss`1=e by A107,A115;
hence contradiction by A113;
end;
s4<=s0 by A5,A6,A7,A23,A22,A71,A103,A105,JORDAN5C:def 3;
hence contradiction by A72,A103,A108,XXREAL_0:1;
end;
now
assume ex p51 being Point of TOP-REAL 2 st LE p4,p51,P,p1,p2 & LE
p51,p9,P,p1,p2 & p51`1>e;
then consider p51 being Point of TOP-REAL 2 such that
A116: LE p4,p51,P,p1,p2 and
A117: LE p51,p9,P,p1,p2 and
A118: p51`1>e;
A119: for p5 being Point of TOP-REAL 2 st LE p51,p5,P,p1,p2 & LE p5,
p,P,p1,p2 holds p5`1>=e
proof
let p5 be Point of TOP-REAL 2;
assume that
A120: LE p51,p5,P,p1,p2 and
A121: LE p5,p,P,p1,p2;
A122: LE p4,p5,P,p1,p2 by A116,A120,JORDAN5C:13;
A123: p5 in P by A120,JORDAN5C:def 3;
then
A124: p5=p9 implies LE p9,p5,P,p1,p2 by JORDAN5C:9;
now
per cases by A1,A74,A123,A124,JORDAN5C:14;
case
LE p5,p9,P,p1,p2;
hence thesis by A100,A122;
end;
case
LE p9,p5,P,p1,p2;
hence thesis by A29,A121;
end;
end;
hence thesis;
end;
LE p51,p,P,p1,p2 by A24,A117,JORDAN5C:13;
hence p is_Rin P,p1,p2,e by A1,A3,A4,A118,A119;
end;
hence p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e by A101;
end;
end;
hence p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e;
end;
hence thesis;
end;
theorem
for P being non empty Subset of TOP-REAL 2, p1,p2,p being Point of
TOP-REAL 2,e being Real st P is_an_arc_of p1,p2 & p2`1>e & p in P & p`1=e holds
p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e or p is_OSout P,p1,p2,e
proof
let P be non empty Subset of TOP-REAL 2, p1,p2,p be Point of TOP-REAL 2,e be
Real;
assume that
A1: P is_an_arc_of p1,p2 and
A2: p2`1>e and
A3: p in P and
A4: p`1=e;
now
reconsider pr1a=proj1 as Function of TOP-REAL 2,R^1 by TOPMETR:17;
reconsider pro1=pr1a|P as Function of (TOP-REAL 2)|P,R^1 by PRE_TOPC:9;
consider f being Function of I[01], (TOP-REAL 2)|P such that
A5: f is being_homeomorphism and
A6: f.0 = p1 and
A7: f.1 = p2 by A1,TOPREAL1:def 1;
A8: f is continuous by A5,TOPS_2:def 5;
A9: rng f=[#]((TOP-REAL 2)|P) by A5,TOPS_2:def 5;
then p in rng f by A3,PRE_TOPC:def 5;
then consider xs being object such that
A10: xs in dom f and
A11: p=f.xs by FUNCT_1:def 3;
A12: dom f=[#](I[01]) by A5,TOPS_2:def 5;
reconsider s2=xs as Real by A10;
A13: s2<=1 by A10,BORSUK_1:40,XXREAL_1:1;
for q being Point of TOP-REAL 2 st q=f.1 holds q`1<>e by A2,A7;
then
A14: 1 in {s where s is Real: 1>=s & s>=s2 & (for q being Point of
TOP-REAL 2 st q=f.s holds q`1<>e)} by A13;
{s where s is Real: 1>=s & s>=s2 &
for q being Point of TOP-REAL 2 st q=f.s holds q`1<>e } c= REAL
proof
let x be object;
assume x in {s where s is Real: 1>=s & s>=s2 &
(for q being Point of TOP-REAL 2 st q=f.s holds q`1<>e)};
then consider s being Real such that
A15: s=x & 1>=s & s>=s2 &
for q being Point of TOP-REAL 2 st q=f.s holds q`1<>e;
s in REAL by XREAL_0:def 1;
hence thesis by A15;
end;
then reconsider R={s where s is Real: 1>=s & s>=s2 &
(for q being Point of
TOP-REAL 2 st q=f.s holds q`1<>e)} as non empty Subset of REAL by A14;
reconsider s0=lower_bound R as Real;
A16: for s being Real st s in R holds s > s2
proof
let s be Real;
assume s in R;
then
A17: ex s3 being Real st s3=s & 1>=s3 & s3>=s2 & for q being Point of
TOP-REAL 2 st q=f.s3 holds q`1<>e;
then s<>s2 by A4,A11;
hence thesis by A17,XXREAL_0:1;
end;
then for s being Real st s in R holds s >= s2;
then
A18: s0 >= s2 by SEQ_4:43;
for p7 being Point of (TOP-REAL 2)|P holds pro1.p7=proj1.p7
proof
let p7 be Point of (TOP-REAL 2)|P;
the carrier of ((TOP-REAL 2)|P)=P by PRE_TOPC:8;
hence thesis by FUNCT_1:49;
end;
then
A19: pro1 is continuous by JGRAPH_2:29;
reconsider h=pro1*f as Function of I[01],R^1;
A20: dom h=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
for s being ExtReal st s in R holds s >= s2 by A16;
then s2 is LowerBound of R by XXREAL_2:def 2;
then
A21: R is bounded_below by XXREAL_2:def 9;
A22: 0<=s2 by A10,BORSUK_1:40,XXREAL_1:1;
R c= [.0,1.]
proof
let x be object;
assume x in R;
then ex s being Real st s=x & 1>=s & s>=s2 &
for q being Point of
TOP-REAL 2 st q=f.s holds q`1<>e;
hence thesis by A22,XXREAL_1:1;
end;
then
A23: 1 >= s0 by A14,BORSUK_1:40,BORSUK_4:26;
then s0 in dom f by A12,A22,A18,BORSUK_1:40,XXREAL_1:1;
then f.s0 in rng f by FUNCT_1:def 3;
then f.s0 in P by A9,PRE_TOPC:def 5;
then reconsider p9=f.s0 as Point of TOP-REAL 2;
A24: LE p,p9,P,p1,p2 by A1,A5,A6,A7,A11,A22,A13,A23,A18,JORDAN5C:8;
A25: rng f=P by A9,PRE_TOPC:def 5;
A26: for p8 being Point of TOP-REAL 2 st LE p8,p9,P,p1,p2 & LE p,p8,P,p1,
p2 holds p8`1=e
proof
let p8 be Point of TOP-REAL 2;
assume that
A27: LE p8,p9,P,p1,p2 and
A28: LE p,p8,P,p1,p2;
A29: p8 in P by A27,JORDAN5C:def 3;
then consider x8 being object such that
A30: x8 in dom f and
A31: p8=f.x8 by A25,FUNCT_1:def 3;
reconsider s8=x8 as Element of REAL by A12,A30,BORSUK_1:40;
A32: s8<=1 by A30,BORSUK_1:40,XXREAL_1:1;
0<=s8 by A30,BORSUK_1:40,XXREAL_1:1;
then
A33: s8>=s2 by A5,A6,A7,A11,A13,A28,A31,A32,JORDAN5C:def 3;
A34: s0>=s8 by A5,A6,A7,A22,A23,A18,A27,A31,A32,JORDAN5C:def 3;
now
reconsider s8n=s8 as Point of RealSpace by METRIC_1:def 13;
reconsider s8m=s8 as Point of Closed-Interval-MSpace(0,1) by A30,
BORSUK_1:40,TOPMETR:10;
reconsider ee=|.p8`1-e.|/2 as Real;
reconsider w=p8`1 as Element of RealSpace
by METRIC_1:def 13,XREAL_0:def 1;
reconsider B=Ball(w,ee) as Subset of R^1 by METRIC_1:def 13,TOPMETR:17;
A35: B={s7 where s7 is Real:p8`1-ee<s7 & s7<p8`1+ee} by JORDAN2B:17
.= ].p8`1-ee,p8`1+ee.[ by RCOMP_1:def 2;
assume
A36: p8`1<>e;
then p8`1-e<>0;
then |.p8`1-e.|>0 by COMPLEX1:47;
then
A37: w in Ball(w,ee) by GOBOARD6:1,XREAL_1:139;
A38: h"B is open & I[01]=TopSpaceMetr(Closed-Interval-MSpace(0,1)) by A8,A19
,TOPMETR:20,def 6,def 7,UNIFORM1:2;
h.s8=pro1.(f.s8) by A20,A30,BORSUK_1:40,FUNCT_1:12
.=proj1.p8 by A29,A31,FUNCT_1:49
.=p8`1 by PSCOMP_1:def 5;
then s8 in h"B by A20,A30,A37,BORSUK_1:40,FUNCT_1:def 7;
then consider r0 being Real such that
A39: r0>0 and
A40: Ball(s8m,r0) c= h"B by A38,TOPMETR:15;
reconsider r0 as Real;
reconsider r01=min(s8-s2,r0) as Real;
the carrier of Closed-Interval-MSpace(0,1)=[.0,1.] & Ball(s8n,r01
)= (].s8- r01,s8+r01 .[) by FRECHET:7,TOPMETR:10;
then
A41: Ball(s8m,r01)= (].s8-r01,s8+r01 .[) /\ [.0,1.] by TOPMETR:9;
s8>s2 by A4,A11,A31,A33,A36,XXREAL_0:1;
then s8-s2>0 by XREAL_1:50;
then
A42: r01>0 by A39,XXREAL_0:21;
then
A43: r01-r01/2+r01/2>0+r01/2 by XREAL_1:6;
then
A44: s8-r01<s8-r01/2 by XREAL_1:10;
A45: r01/2>0 by A42,XREAL_1:139;
then
A46: s8+-(r01/2)<s8+r01/2 by XREAL_1:8;
s8+r01/2<s8+r01 by A43,XREAL_1:8;
then s8-r01/2<s8+r01 by A46,XXREAL_0:2;
then
A47: s8-r01/2 in ].s8-r01,s8+r01 .[ by A44,XXREAL_1:4;
A48: s8-r01/2>s8-r01 by A43,XREAL_1:10;
Ball(s8m,r01) c= Ball(s8m,r0) by PCOMPS_1:1,XXREAL_0:17;
then
A49: (].s8-r01,s8+r01 .[)/\ [.0,1.] c= h"B by A40,A41;
reconsider s70=s8-r01/2 as Real;
s8-s2>=r01 by XXREAL_0:17;
then -(s8-s2)<= -r01 by XREAL_1:24;
then
A50: s2-s8+s8<= -r01+s8 by XREAL_1:7;
--(r01/2)> 0 by A42,XREAL_1:139;
then -(r01/2) < 0;
then
A51: s8+0>s8+-r01/2 by XREAL_1:8;
then
A52: 1>=s70 by A32,XXREAL_0:2;
1-0>s8-r01/2 by A32,A45,XREAL_1:15;
then s8-r01/2 in [.0,1.] by A22,A50,A48,XXREAL_1:1;
then
A53: s8-r01/2 in (].s8-r01,s8+r01 .[)/\ [.0,1.] by A47,XBOOLE_0:def 4;
then
A54: h.(s8-r01/2) in B by A49,FUNCT_1:def 7;
A55: s8-r01/2 in dom h by A49,A53,FUNCT_1:def 7;
A56: for p7 being Point of TOP-REAL 2 st p7=f.s70 holds p7`1<>e
proof
let p7 be Point of TOP-REAL 2;
assume
A57: p7=f.s70;
s70 in [.0,1.] by A22,A50,A44,A52,XXREAL_1:1;
then
A58: p7 in rng f by A12,A57,BORSUK_1:40,FUNCT_1:def 3;
A59: rng f=[#]((TOP-REAL 2)|P) by A5,TOPS_2:def 5
.=P by PRE_TOPC:def 5;
A60: h.s70=pro1.(f.s70) by A55,FUNCT_1:12
.=pr1a.(p7) by A57,A58,A59,FUNCT_1:49
.=p7`1 by PSCOMP_1:def 5;
then
A61: p7`1<p8`1+ee by A35,A54,XXREAL_1:4;
A62: p8`1-ee<p7`1 by A35,A54,A60,XXREAL_1:4;
now
assume
A63: p7`1=e;
now
per cases;
case
A64: p8`1-e>=0;
then p8`1-(p8`1-e)/2<e by A62,A63,ABSVALUE:def 1;
then p8`1/2+e/2<e/2+e/2;
then p8`1/2<e/2 by XREAL_1:7;
then
A65: p8`1/2-e/2<e/2-e/2 by XREAL_1:14;
(p8`1-e)/2>=0/2 by A64;
hence contradiction by A65;
end;
case
A66: p8`1-e<0;
then e< p8`1+(-(p8`1-e))/2 by A61,A63,ABSVALUE:def 1;
then p8`1/2+e/2>e/2+e/2;
then p8`1/2>e/2 by XREAL_1:7;
then
A67: p8`1/2-e/2>e/2-e/2 by XREAL_1:14;
(p8`1-e)/2<=0/2 by A66;
hence contradiction by A67;
end;
end;
hence contradiction;
end;
hence thesis;
end;
s70>=s2 by A50,A44,XXREAL_0:2;
then consider s7 being Real such that
A68: s8>s7 and
A69: 1>=s7 & s7>=s2 & for p7 being Point of TOP-REAL 2 st p7=f.s7
holds p7`1 <>e by A51,A52,A56;
s7 in R by A69;
then s7 >=s0 by A21,SEQ_4:def 2;
hence contradiction by A34,A68,XXREAL_0:2;
end;
hence thesis;
end;
assume not p is_OSout P,p1,p2,e;
then consider p4 being Point of TOP-REAL 2 such that
A70: LE p9,p4,P,p1,p2 and
A71: p4<>p9 and
A72: (for p5 being Point of TOP-REAL 2 st LE p5,p4,P,p1,p2 & LE p9,p5
, P,p1,p2 holds p5`1<=e)or for p6 being Point of TOP-REAL 2 st LE p6,p4,P,p1,p2
& LE p9,p6,P,p1,p2 holds p6`1>=e by A1,A3,A4,A24,A26;
A73: p9 in P by A70,JORDAN5C:def 3;
now
per cases by A72;
case
A74: for p5 being Point of TOP-REAL 2 st LE p5,p4,P,p1,p2 & LE p9
,p5,P,p1,p2 holds p5`1<=e;
A75: now
p4 in P by A70,JORDAN5C:def 3;
then p4 in rng f by A9,PRE_TOPC:def 5;
then consider xs4 being object such that
A76: xs4 in dom f and
A77: p4=f.xs4 by FUNCT_1:def 3;
reconsider s4=xs4 as Real by A76;
A78: s4<=1 by A76,BORSUK_1:40,XXREAL_1:1;
assume
A79: not ex p51 being Point of TOP-REAL 2 st LE p51,p4,P,p1,p2
& LE p9,p51,P,p1,p2 & p51`1<e;
A80: for p51 being Point of TOP-REAL 2 st LE p51,p4,P,p1,p2 & LE p9
,p51,P,p1,p2 holds p51`1=e
proof
let p51 be Point of TOP-REAL 2;
assume LE p51,p4,P,p1,p2 & LE p9,p51,P,p1,p2;
then p51`1>=e & p51`1<=e by A74,A79;
hence thesis by XXREAL_0:1;
end;
A81: now
assume s4>s0;
then --(s4-s0)>0 by XREAL_1:50;
then -(s4-s0)<0;
then
A82: (s0-s4)/2<0 by XREAL_1:141;
then -((s0-s4)/2)>0 by XREAL_1:58;
then consider r being Real such that
A83: r in R and
A84: r<s0+(-((s0-s4)/2)) by A21,SEQ_4:def 2;
reconsider rss=r as Real;
A85: ex s7 being Real st s7=r & 1>=s7 & s7>=s2 &
for q being Point
of TOP-REAL 2 st q=f.s7 holds q`1<>e by A83;
then r in [.0,1.] by A22,XXREAL_1:1;
then f.rss in rng f by A12,BORSUK_1:40,FUNCT_1:def 3;
then f.rss in P by A9,PRE_TOPC:def 5;
then reconsider pss=f.rss as Point of TOP-REAL 2;
s4+0>s4+(s0-s4)/2 by A82,XREAL_1:8;
then
A86: s4>r by A84,XXREAL_0:2;
then
A87: 1>r by A78,XXREAL_0:2;
A88: r>=s0 by A21,A83,SEQ_4:def 2;
then
A89: LE p9,pss,P,p1,p2 by A1,A5,A6,A7,A22,A23,A18,A87,JORDAN5C:8;
LE pss,p4,P,p1,p2 by A1,A5,A6,A7,A22,A18,A77,A78,A88,A86,A87,
JORDAN5C:8;
then pss`1=e by A80,A89;
hence contradiction by A85;
end;
0<=s4 by A76,BORSUK_1:40,XXREAL_1:1;
then s4>=s0 by A5,A6,A7,A23,A70,A77,A78,JORDAN5C:def 3;
hence contradiction by A71,A77,A81,XXREAL_0:1;
end;
now
assume ex p51 being Point of TOP-REAL 2 st LE p51,p4,P,p1,p2 & LE
p9,p51,P,p1,p2 & p51`1<e;
then consider p51 being Point of TOP-REAL 2 such that
A90: LE p51,p4,P,p1,p2 and
A91: LE p9,p51,P,p1,p2 and
A92: p51`1<e;
A93: for p5 being Point of TOP-REAL 2 st LE p5,p51,P,p1,p2 & LE p,
p5,P,p1,p2 holds p5`1<=e
proof
let p5 be Point of TOP-REAL 2;
assume that
A94: LE p5,p51,P,p1,p2 and
A95: LE p,p5,P,p1,p2;
A96: LE p5,p4,P,p1,p2 by A90,A94,JORDAN5C:13;
A97: p5 in P by A94,JORDAN5C:def 3;
then
A98: p5=p9 implies LE p9,p5,P,p1,p2 by JORDAN5C:9;
now
per cases by A1,A73,A97,A98,JORDAN5C:14;
case
LE p5,p9,P,p1,p2;
hence thesis by A26,A95;
end;
case
LE p9,p5,P,p1,p2;
hence thesis by A74,A96;
end;
end;
hence thesis;
end;
LE p,p51,P,p1,p2 by A24,A91,JORDAN5C:13;
hence p is_Lout P,p1,p2,e by A1,A3,A4,A92,A93;
end;
hence p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e by A75;
end;
case
A99: for p6 being Point of TOP-REAL 2 st LE p6,p4,P,p1,p2 & LE p9
,p6,P,p1,p2 holds p6`1>=e;
A100: now
p4 in P by A70,JORDAN5C:def 3;
then p4 in rng f by A9,PRE_TOPC:def 5;
then consider xs4 being object such that
A101: xs4 in dom f and
A102: p4=f.xs4 by FUNCT_1:def 3;
reconsider s4=xs4 as Real by A101;
A103: s4<=1 by A101,BORSUK_1:40,XXREAL_1:1;
assume
A104: not ex p51 being Point of TOP-REAL 2 st LE p51,p4,P,p1,p2
& LE p9,p51,P,p1,p2 & p51`1>e;
A105: for p51 being Point of TOP-REAL 2 st LE p51,p4,P,p1,p2 & LE p9
,p51,P,p1,p2 holds p51`1=e
proof
let p51 be Point of TOP-REAL 2;
assume LE p51,p4,P,p1,p2 & LE p9,p51,P,p1,p2;
then p51`1<=e & p51`1>=e by A99,A104;
hence thesis by XXREAL_0:1;
end;
A106: now
assume s4>s0;
then --(s4-s0)>0 by XREAL_1:50;
then -(s4-s0)<0;
then
A107: (s0-s4)/2<0 by XREAL_1:141;
then -((s0-s4)/2)>0 by XREAL_1:58;
then consider r being Real such that
A108: r in R and
A109: r<s0+(-((s0-s4)/2)) by A21,SEQ_4:def 2;
reconsider rss=r as Real;
A110: ex s7 being Real st s7=r & 1>=s7 & s7>=s2 &
for q being Point
of TOP-REAL 2 st q=f.s7 holds q`1<>e by A108;
then r in [.0,1.] by A22,XXREAL_1:1;
then f.rss in rng f by A12,BORSUK_1:40,FUNCT_1:def 3;
then f.rss in P by A9,PRE_TOPC:def 5;
then reconsider pss=f.rss as Point of TOP-REAL 2;
s4+0>s4+(s0-s4)/2 by A107,XREAL_1:8;
then
A111: s4>r by A109,XXREAL_0:2;
then
A112: 1>r by A103,XXREAL_0:2;
A113: r>=s0 by A21,A108,SEQ_4:def 2;
then
A114: LE p9,pss,P,p1,p2 by A1,A5,A6,A7,A22,A23,A18,A112,JORDAN5C:8;
LE pss,p4,P,p1,p2 by A1,A5,A6,A7,A22,A18,A102,A103,A113,A111,A112,
JORDAN5C:8;
then pss`1=e by A105,A114;
hence contradiction by A110;
end;
0<=s4 by A101,BORSUK_1:40,XXREAL_1:1;
then s4>=s0 by A5,A6,A7,A23,A70,A102,A103,JORDAN5C:def 3;
hence contradiction by A71,A102,A106,XXREAL_0:1;
end;
now
assume ex p51 being Point of TOP-REAL 2 st LE p51,p4,P,p1,p2 & LE
p9,p51,P,p1,p2 & p51`1>e;
then consider p51 being Point of TOP-REAL 2 such that
A115: LE p51,p4,P,p1,p2 and
A116: LE p9,p51,P,p1,p2 and
A117: p51`1>e;
A118: for p5 being Point of TOP-REAL 2 st LE p5,p51,P,p1,p2 & LE p,
p5,P,p1,p2 holds p5`1>=e
proof
let p5 be Point of TOP-REAL 2;
assume that
A119: LE p5,p51,P,p1,p2 and
A120: LE p,p5,P,p1,p2;
A121: LE p5,p4,P,p1,p2 by A115,A119,JORDAN5C:13;
A122: p5 in P by A119,JORDAN5C:def 3;
then
A123: p5=p9 implies LE p9,p5,P,p1,p2 by JORDAN5C:9;
now
per cases by A1,A73,A122,A123,JORDAN5C:14;
case
LE p9,p5,P,p1,p2;
hence thesis by A99,A121;
end;
case
LE p5,p9,P,p1,p2;
hence thesis by A26,A120;
end;
end;
hence thesis;
end;
LE p,p51,P,p1,p2 by A24,A116,JORDAN5C:13;
hence p is_Rout P,p1,p2,e by A1,A3,A4,A117,A118;
end;
hence p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e by A100;
end;
end;
hence p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e;
end;
hence thesis;
end;
theorem Th11:
for P being Subset of I[01],s being Real st P=[.0,s.[
holds P is open
proof
A1: [#]I[01]=[.0,1.] by TOPMETR:18,20;
let P be Subset of I[01],s be Real;
assume
A2: P=[.0,s.[;
per cases;
suppose
A3: s in [.0,1.];
reconsider T=[.0,1.] as Subset of R^1 by TOPMETR:17;
0 in [.0,1.] by XXREAL_1:1;
then [.0,s.[ c= [.0,s.] & [.0,s.] c= [.0,1.] by A3,XXREAL_1:24
,XXREAL_2:def 12;
then [.0,s.[ c= [.0,1.];
then P c= [#](R^1|T) by A2,PRE_TOPC:def 5;
then reconsider P2=P as Subset of R^1|T;
reconsider Q=].-1,s.[ as Subset of R^1 by TOPMETR:17;
A4: s<=1 by A3,XXREAL_1:1;
A5: [.0,s.[ c= ].-1,s.[ /\ [.0,1.]
proof
let x be object;
assume
A6: x in [.0,s.[;
then reconsider sx=x as Real;
A7: 0<=sx by A6,XXREAL_1:3;
A8: sx<s by A6,XXREAL_1:3;
then sx<=1 by A4,XXREAL_0:2;
then
A9: x in [.0,1.] by A7,XXREAL_1:1;
-1 < sx by A7,XXREAL_0:2;
then x in ].-1,s.[ by A8,XXREAL_1:4;
hence thesis by A9,XBOOLE_0:def 4;
end;
].-1,s.[ /\ [.0,1.] c= [.0,s.[
proof
let x be object;
assume
A10: x in ].-1,s.[ /\ [.0,1.];
then reconsider sx=x as Real;
x in [.0,1.] by A10,XBOOLE_0:def 4;
then
A11: 0<=sx by XXREAL_1:1;
x in ].-1,s.[ by A10,XBOOLE_0:def 4;
then sx<s by XXREAL_1:4;
hence thesis by A11,XXREAL_1:3;
end;
then [.0,s.[ = ].-1,s.[ /\ [.0,1.] by A5,XBOOLE_0:def 10;
then
A12: P2=Q /\ [#](R^1|T) by A2,PRE_TOPC:def 5;
Q is open & Closed-Interval-TSpace(0,1) =R^1|T by JORDAN6:35,TOPMETR:19;
hence thesis by A12,TOPMETR:20,TOPS_2:24;
end;
suppose
A13: not s in [.0,1.];
now
per cases by A13,XXREAL_1:1;
case
s<0;
then [.0,s.[ ={} by XXREAL_1:27;
then P in the topology of I[01] by A2,PRE_TOPC:1;
hence thesis by PRE_TOPC:def 2;
end;
case
A14: s>1;
A15: for r being Real st 0<=r & r<s holds r<=1
proof
let r be Real;
assume 0<=r & r<s;
then r in [.0,s.[ by XXREAL_1:3;
hence thesis by A2,A1,XXREAL_1:1;
end;
consider t being Real such that
A16: 1<t and
A17: t<s by A14,XREAL_1:5;
reconsider t as Real;
thus contradiction by A16,A17,A15;
end;
end;
hence thesis;
end;
end;
theorem Th12:
for P being Subset of I[01],s being Real st P=].s,1.] holds P is open
proof
A1: [#]I[01]=[.0,1.] by TOPMETR:18,20;
let P be Subset of I[01],s be Real;
assume
A2: P=].s,1.];
per cases;
suppose
A3: s in [.0,1.];
reconsider T=[.0,1.] as Subset of R^1 by TOPMETR:17;
1 in [.0,1.] by XXREAL_1:1;
then ].s,1.] c= [.s,1.] & [.s,1.] c= [.0,1.] by A3,XXREAL_1:23
,XXREAL_2:def 12;
then ].s,1.] c= [.0,1.];
then P c= [#](R^1|T) by A2,PRE_TOPC:def 5;
then reconsider P2=P as Subset of R^1|T;
reconsider Q=].s,2.[ as Subset of R^1 by TOPMETR:17;
A4: 0<=s by A3,XXREAL_1:1;
A5: ].s,1.] c= ].s,2.[ /\ [.0,1.]
proof
let x be object;
assume
A6: x in ].s,1.];
then reconsider sx=x as Real;
A7: s<sx by A6,XXREAL_1:2;
A8: sx<=1 by A6,XXREAL_1:2;
then 2 > sx by XXREAL_0:2;
then
A9: x in ].s,2.[ by A7,XXREAL_1:4;
x in [.0,1.] by A4,A7,A8,XXREAL_1:1;
hence thesis by A9,XBOOLE_0:def 4;
end;
].s,2.[ /\ [.0,1.] c= ].s,1.]
proof
let x be object;
assume
A10: x in ].s,2.[ /\ [.0,1.];
then reconsider sx=x as Real;
x in [.0,1.] by A10,XBOOLE_0:def 4;
then
A11: sx<=1 by XXREAL_1:1;
x in ].s,2.[ by A10,XBOOLE_0:def 4;
then s<sx by XXREAL_1:4;
hence thesis by A11,XXREAL_1:2;
end;
then ].s,1.] = ].s,2.[ /\ [.0,1.] by A5,XBOOLE_0:def 10;
then
A12: P2=Q /\ [#](R^1|T) by A2,PRE_TOPC:def 5;
Q is open & Closed-Interval-TSpace(0,1) =R^1|T by JORDAN6:35,TOPMETR:19;
hence thesis by A12,TOPMETR:20,TOPS_2:24;
end;
suppose
A13: not s in [.0,1.];
now
per cases by A13,XXREAL_1:1;
case
s>1;
then ].s,1.] ={} by XXREAL_1:26;
then P in the topology of I[01] by A2,PRE_TOPC:1;
hence thesis by PRE_TOPC:def 2;
end;
case
A14: s<0;
A15: for r being Real st s<r & r<=1 holds r>=0
proof
let r be Real;
assume s<r & r<=1;
then r in ].s,1.] by XXREAL_1:2;
hence thesis by A2,A1,XXREAL_1:1;
end;
consider t being Real such that
A16: s<t and
A17: t<0 by A14,XREAL_1:5;
reconsider t as Real;
thus contradiction by A16,A17,A15;
end;
end;
hence thesis;
end;
end;
theorem Th13:
for P being non empty Subset of TOP-REAL 2, P1 being Subset of (
TOP-REAL 2)|P,Q being Subset of I[01], f being Function of I[01],(TOP-REAL 2)|P
,s being Real st s<=1 & P1= {q0 where q0 is Point of TOP-REAL 2:
ex ss being
Real st 0<=ss & ss<s & q0=f.ss} & Q=[.0,s.[ holds f.:Q=P1
proof
let P be non empty Subset of TOP-REAL 2, P1 be Subset of (TOP-REAL 2)|P, Q
be Subset of I[01], f be Function of I[01],(TOP-REAL 2)|P,
s be Real;
assume that
A1: s<=1 and
A2: P1= {q0 where q0 is Point of TOP-REAL 2:
ex ss being Real st 0<=ss &
ss<s & q0=f.ss} and
A3: Q=[.0,s.[;
A4: the carrier of (TOP-REAL 2)|P=P by PRE_TOPC:8;
A5: f.:Q c= P1
proof
let y be object;
assume y in f.:Q;
then consider z being object such that
A6: z in dom f and
A7: z in Q and
A8: f.z=y by FUNCT_1:def 6;
reconsider ss=z as Real by A6;
y in rng f by A6,A8,FUNCT_1:def 3;
then y in P by A4;
then reconsider q=y as Point of TOP-REAL 2;
0<=ss & ss<s by A3,A7,XXREAL_1:3;
then ex ss being Real st 0<=ss & ss<s & q=f.ss by A8;
hence thesis by A2;
end;
P1 c= f.:Q
proof
let x be object;
A9: dom f= [.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
assume x in P1;
then consider q0 being Point of TOP-REAL 2 such that
A10: q0=x and
A11: ex ss being Real st 0<=ss & ss<s & q0=f.ss by A2;
consider ss being Real such that
A12: 0<=ss and
A13: ss<s and
A14: q0=f.ss by A11;
ss<1 by A1,A13,XXREAL_0:2;
then
A15: ss in dom f by A12,A9,XXREAL_1:1;
ss in Q by A3,A12,A13,XXREAL_1:3;
hence thesis by A10,A14,A15,FUNCT_1:def 6;
end;
hence thesis by A5,XBOOLE_0:def 10;
end;
theorem Th14:
for P being non empty Subset of TOP-REAL 2, P1 being Subset of (
TOP-REAL 2)|P,Q being Subset of I[01], f being Function of I[01],(TOP-REAL 2)|P
,s being Real st s>=0 & P1= {q0 where q0 is Point of TOP-REAL 2:
ex ss being Real
st s<ss & ss<=1 & q0=f.ss} & Q=].s,1.] holds f.:Q=P1
proof
let P be non empty Subset of TOP-REAL 2, P1 be Subset of (TOP-REAL 2)|P, Q
be Subset of I[01], f be Function of I[01],(TOP-REAL 2)|P,
s be Real;
assume that
A1: s>=0 and
A2: P1= {q0 where q0 is Point of TOP-REAL 2:
ex ss being Real st s<ss &
ss<=1 & q0=f.ss} and
A3: Q=].s,1.];
A4: the carrier of (TOP-REAL 2)|P=P by PRE_TOPC:8;
A5: f.:Q c= P1
proof
let y be object;
assume y in f.:Q;
then consider z being object such that
A6: z in dom f and
A7: z in Q and
A8: f.z=y by FUNCT_1:def 6;
reconsider ss=z as Real by A6;
y in rng f by A6,A8,FUNCT_1:def 3;
then y in P by A4;
then reconsider q=y as Point of TOP-REAL 2;
s<ss & ss<=1 by A3,A7,XXREAL_1:2;
then ex ss being Real st s<ss & ss<=1 & q=f.ss by A8;
hence thesis by A2;
end;
P1 c= f.:Q
proof
let x be object;
assume x in P1;
then consider q0 being Point of TOP-REAL 2 such that
A9: q0=x and
A10: ex ss being Real st s<ss & ss<=1 & q0=f.ss by A2;
consider ss being Real such that
A11: s<ss & ss<=1 and
A12: q0=f.ss by A10;
A13: ss in Q by A3,A11,XXREAL_1:2;
dom f= [.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
then ss in dom f by A1,A11,XXREAL_1:1;
hence thesis by A9,A12,A13,FUNCT_1:def 6;
end;
hence thesis by A5,XBOOLE_0:def 10;
end;
Lm1: [#]I[01]<> {};
theorem Th15:
for P being non empty Subset of TOP-REAL 2, P1 being Subset of (
TOP-REAL 2)|P, f being Function of I[01],(TOP-REAL 2)|P,
s being Real st s<=1 &
f is being_homeomorphism &
P1= {q0 where q0 is Point of TOP-REAL 2: ex ss being
Real st 0<=ss & ss<s & q0=f.ss} holds P1 is open
proof
let P be non empty Subset of TOP-REAL 2, P1 be Subset of (TOP-REAL 2)|P, f
be Function of I[01],(TOP-REAL 2)|P,s be Real;
assume that
A1: s<=1 and
A2: f is being_homeomorphism and
A3: P1= {q0 where q0 is Point of TOP-REAL 2:
ex ss being Real st 0<=ss &
ss<s & q0=f.ss};
f is one-to-one & rng f=[#]((TOP-REAL 2)|P) by A2,TOPS_2:def 5;
then
A4: (f")"=f by TOPS_2:51;
[.0,s.[ c= [.0,1.]
proof
let x be object;
assume
A5: x in [.0,s.[;
then reconsider sx=x as Real;
sx<s by A5,XXREAL_1:3;
then
A6: sx<1 by A1,XXREAL_0:2;
0<=sx by A5,XXREAL_1:3;
hence thesis by A6,XXREAL_1:1;
end;
then reconsider Q=[.0,s.[ as Subset of I[01] by TOPMETR:18,20;
A7: Q is open by Th11;
A8: f" is being_homeomorphism by A2,TOPS_2:56;
then
A9: f" is one-to-one by TOPS_2:def 5;
rng (f") =[#](I[01]) by A8,TOPS_2:def 5;
then f" is onto by FUNCT_2:def 3;
then (f")"=(f" qua Function)" by A9,TOPS_2:def 4;
then
A10: ((f")").:Q=(f")"Q by A9,FUNCT_1:85;
A11: P1=f.:Q by A1,A3,Th13;
f" is continuous by A2,TOPS_2:def 5;
hence thesis by A7,A4,A10,Lm1,A11,TOPS_2:43;
end;
theorem Th16:
for P being non empty Subset of TOP-REAL 2, P1 being Subset of (
TOP-REAL 2)|P, f being Function of I[01],(TOP-REAL 2)|P,
s being Real st s>=0 &
f is being_homeomorphism & P1= {q0 where q0 is Point of TOP-REAL 2: ex ss being
Real st s<ss & ss<=1 & q0=f.ss} holds P1 is open
proof
let P be non empty Subset of TOP-REAL 2, P1 be Subset of (TOP-REAL 2)|P, f
be Function of I[01],(TOP-REAL 2)|P,s be Real;
assume that
A1: s>=0 and
A2: f is being_homeomorphism and
A3: P1= {q0 where q0 is Point of TOP-REAL 2:
ex ss being Real st s<ss &
ss<=1 & q0=f.ss};
f is one-to-one & rng f=[#]((TOP-REAL 2)|P) by A2,TOPS_2:def 5;
then
A4: (f")"=f by TOPS_2:51;
].s,1.] c= [.0,1.]
proof
let x be object;
assume
A5: x in ].s,1.];
then reconsider sx=x as Real;
0<sx & sx<=1 by A1,A5,XXREAL_1:2;
hence thesis by XXREAL_1:1;
end;
then reconsider Q=].s,1.] as Subset of I[01] by TOPMETR:18,20;
A6: [#]I[01] <> {} & Q is open by Th12;
A7: f" is being_homeomorphism by A2,TOPS_2:56;
then
A8: f" is one-to-one by TOPS_2:def 5;
rng (f") =[#](I[01]) by A7,TOPS_2:def 5;
then f" is onto by FUNCT_2:def 3;
then (f")"=(f" qua Function)" by A8,TOPS_2:def 4;
then
A9: ((f")").:Q=(f")"Q by A8,FUNCT_1:85;
P1=f.:Q & f" is continuous by A1,A2,A3,Th14,TOPS_2:def 5;
hence thesis by A6,A4,A9,TOPS_2:43;
end;
theorem Th17:
for T being non empty TopStruct, Q1,Q2 being Subset of T, p1,p2
being Point of T st Q1 /\ Q2={} & Q1 \/ Q2=the carrier of T & p1 in Q1 & p2 in
Q2 & Q1 is open & Q2 is open holds not ex P being Function of I[01],T st P is
continuous & P.0=p1 & P.1=p2
proof
let T be non empty TopStruct, Q1,Q2 be Subset of T, p1,p2 be Point of T;
assume that
A1: Q1 /\ Q2={} and
A2: Q1 \/ Q2=the carrier of T and
A3: p1 in Q1 and
A4: p2 in Q2 and
A5: Q1 is open & Q2 is open;
assume ex P being Function of I[01],T st P is continuous & P.0=p1 & P.1=p2;
then consider P being Function of I[01],T such that
A6: P is continuous and
A7: P.0=p1 and
A8: P.1=p2;
[#]T <> {};
then
A9: P"Q1 is open & P"Q2 is open by A5,A6,TOPS_2:43;
A10: [#]I[01]=[.0,1.] by TOPMETR:18,20;
then 0 in the carrier of I[01] by XXREAL_1:1;
then 0 in dom P by FUNCT_2:def 1;
then
A11: [#]I[01]=the carrier of I[01] & P"Q1 <> {}I[01] by A3,A7,FUNCT_1:def 7;
P"Q1 /\ P"Q2 =P"(Q1 /\ Q2) by FUNCT_1:68
.={} by A1;
then
A12: not P"Q1 meets P"Q2 by XBOOLE_0:def 7;
1 in the carrier of I[01] by A10,XXREAL_1:1;
then 1 in dom P by FUNCT_2:def 1;
then
A13: P"Q2 <> {}I[01] by A4,A8,FUNCT_1:def 7;
P"Q1 \/ P"Q2 =P"(Q1 \/ Q2) by RELAT_1:140
.= the carrier of I[01] by A2,FUNCT_2:40;
hence contradiction by A9,A11,A13,A12,CONNSP_1:11,TREAL_1:19;
end;
theorem Th18:
for P being non empty Subset of TOP-REAL 2, Q being Subset of (
TOP-REAL 2)|P, p1,p2,q being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & q in
P & q<>p1 & q<>p2 & Q=P\{q} holds not Q is connected &
not ex R being Function
of I[01],((TOP-REAL 2)|P)|Q st R is continuous & R.0=p1 & R.1=p2
proof
let P be non empty Subset of TOP-REAL 2, Q be Subset of (TOP-REAL 2)|P, p1,
p2,q be Point of TOP-REAL 2;
assume that
A1: P is_an_arc_of p1,p2 and
A2: q in P and
A3: q<>p1 and
A4: q<>p2 and
A5: Q=P\{q};
consider f being Function of I[01], (TOP-REAL 2)|P such that
A6: f is being_homeomorphism and
A7: f.0 = p1 and
A8: f.1 = p2 by A1,TOPREAL1:def 1;
A9: rng f=[#]((TOP-REAL 2)|P) by A6,TOPS_2:def 5;
A10: [#]I[01]=[.0,1.] by TOPMETR:18,20;
A11: [#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 5;
then consider xs being object such that
A12: xs in dom f and
A13: f.xs=q by A2,A9,FUNCT_1:def 3;
A14: dom f=[#]I[01] by A6,TOPS_2:def 5;
reconsider s=xs as Real by A12;
{q0 where q0 is Point of TOP-REAL 2:
ex ss being Real st s<ss & ss<=1 &
q0=f.ss} c= the carrier of (TOP-REAL 2)|P
proof
let z be object;
assume z in {q0 where q0 is Point of TOP-REAL 2:
ex ss being Real st s<
ss & ss<=1 & q0=f.ss};
then consider q0 being Point of TOP-REAL 2 such that
A15: q0=z and
A16: ex ss being Real st s<ss & ss<=1 & q0=f.ss;
consider ss being Real such that
A17: s<ss and
A18: ss<=1 and
A19: q0=f.ss by A16;
ss>0 by A12,A10,A17,XXREAL_1:1;
then ss in dom f by A14,A10,A18,XXREAL_1:1;
then q0 in rng f by A19,FUNCT_1:def 3;
hence thesis by A15;
end;
then reconsider
P29= {q0 where q0 is Point of TOP-REAL 2:
ex ss being Real st s<
ss & ss<=1 & q0=f.ss} as Subset of (TOP-REAL 2)|P;
A20: 0<=s by A12,A10,XXREAL_1:1;
then
A21: P29 is open by A6,Th16;
A22: P29 c= Q
proof
let x be object;
assume x in P29;
then consider q00 being Point of TOP-REAL 2 such that
A23: q00=x and
A24: ex ss being Real st s<ss & ss<=1 & q00=f.ss;
consider ss being Real such that
A25: s<ss and
A26: ss<=1 and
A27: q00=f.ss by A24;
ss>0 by A12,A10,A25,XXREAL_1:1;
then
A28: ss in dom f by A14,A10,A26,XXREAL_1:1;
now
assume
A29: q00=q;
f is one-to-one by A6,TOPS_2:def 5;
hence contradiction by A12,A13,A25,A27,A28,A29,FUNCT_1:def 4;
end;
then
A30: not q00 in {q} by TARSKI:def 1;
q00 in P by A9,A11,A27,A28,FUNCT_1:def 3;
hence thesis by A5,A23,A30,XBOOLE_0:def 5;
end;
{q0 where q0 is Point of TOP-REAL 2:
ex ss being Real st 0<=ss & ss<s &
q0=f.ss} c= the carrier of (TOP-REAL 2)|P
proof
let z be object;
assume z in {q0 where q0 is Point of TOP-REAL 2:
ex ss being Real st 0<=
ss & ss<s & q0=f.ss};
then consider q0 being Point of TOP-REAL 2 such that
A31: q0=z and
A32: ex ss being Real st 0<=ss & ss<s & q0=f.ss;
consider ss being Real such that
A33: 0<=ss and
A34: ss<s and
A35: q0=f.ss by A32;
s<=1 by A12,A10,XXREAL_1:1;
then ss<1 by A34,XXREAL_0:2;
then ss in dom f by A14,A10,A33,XXREAL_1:1;
then q0 in rng f by A35,FUNCT_1:def 3;
hence thesis by A31;
end;
then reconsider
P19= {q0 where q0 is Point of TOP-REAL 2:
ex ss being Real st 0<=
ss & ss<s & q0=f.ss} as Subset of (TOP-REAL 2)|P;
A36: s<=1 by A12,A10,XXREAL_1:1;
then
A37: P19 is open by A6,Th15;
A38: Q c= P19 \/ P29
proof
let x be object;
assume
A39: x in Q;
then consider xt being object such that
A40: xt in dom f and
A41: f.xt=x by A9,FUNCT_1:def 3;
reconsider t=xt as Real by A40;
A42: t<=1 by A10,A40,XXREAL_1:1;
reconsider qq=x as Point of TOP-REAL 2 by A5,A39;
not x in {q} by A5,A39,XBOOLE_0:def 5;
then
A43: not x=q by TARSKI:def 1;
A44: 0<=t by A10,A40,XXREAL_1:1;
now
per cases;
case
t<s;
then ex ss being Real st 0<=ss & ss<s & qq=f.ss by A41,A44;
then x in P19;
hence thesis by XBOOLE_0:def 3;
end;
case
t>=s;
then t>s by A13,A41,A43,XXREAL_0:1;
then ex ss being Real st s<ss & ss<=1 & qq=f.ss by A41,A42;
then x in P29;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
A45: now
assume P19 meets P29;
then consider p0 being object such that
A46: p0 in P19 and
A47: p0 in P29 by XBOOLE_0:3;
consider q00 being Point of TOP-REAL 2 such that
A48: q00=p0 and
A49: ex ss being Real st 0<=ss & ss<s & q00=f.ss by A46;
consider ss1 being Real such that
A50: 0<=ss1 and
A51: ss1<s and
A52: q00=f.ss1 by A49;
ss1<1 by A36,A51,XXREAL_0:2;
then
A53: ss1 in dom f by A14,A10,A50,XXREAL_1:1;
consider q01 being Point of TOP-REAL 2 such that
A54: q01=p0 and
A55: ex ss being Real st s<ss & ss<=1 & q01=f.ss by A47;
consider ss2 being Real such that
A56: s<ss2 and
A57: ss2<=1 and
A58: q01=f.ss2 by A55;
ss2>0 by A12,A10,A56,XXREAL_1:1;
then
A59: ss2 in dom f by A14,A10,A57,XXREAL_1:1;
f is one-to-one by A6,TOPS_2:def 5;
hence contradiction by A48,A51,A52,A54,A56,A58,A53,A59,FUNCT_1:def 4;
end;
1>s by A4,A8,A13,A36,XXREAL_0:1;
then
A60: p2 in {q0 where q0 is Point of TOP-REAL 2:
ex ss being Real st s<ss &
ss<=1 & q0=f.ss} by A8;
then reconsider Q9=Q as non empty Subset of (TOP-REAL 2)|P by A22;
reconsider T=((TOP-REAL 2)|P)|Q9 as non empty TopSpace;
A61: the carrier of T=[#]T;
then reconsider P299=P29 as Subset of T by A22,PRE_TOPC:def 5;
P29 /\ Q<>{} by A60,A22,XBOOLE_1:28;
then
A62: P29 meets Q by XBOOLE_0:def 7;
A63: P19 c= Q
proof
let x be object;
assume x in P19;
then consider q00 being Point of TOP-REAL 2 such that
A64: q00=x and
A65: ex ss being Real st 0<=ss & ss<s & q00=f.ss;
consider ss being Real such that
A66: 0<=ss and
A67: ss<s and
A68: q00=f.ss by A65;
ss<1 by A36,A67,XXREAL_0:2;
then
A69: ss in dom f by A14,A10,A66,XXREAL_1:1;
now
assume
A70: q00=q;
f is one-to-one by A6,TOPS_2:def 5;
hence contradiction by A12,A13,A67,A68,A69,A70,FUNCT_1:def 4;
end;
then
A71: not q00 in {q} by TARSKI:def 1;
q00 in P by A9,A11,A68,A69,FUNCT_1:def 3;
hence thesis by A5,A64,A71,XBOOLE_0:def 5;
end;
then reconsider P199=P19 as Subset of T by A61,PRE_TOPC:def 5;
P199=P19 /\ (the carrier of T) by XBOOLE_1:28;
then
A72: P199 is open by A37,A61,TOPS_2:24;
s<>0 by A3,A7,A13;
then
A73: p1 in {q0 where q0 is Point of TOP-REAL 2:
ex ss being Real st 0<=ss &
ss<s & q0=f.ss} by A7,A20;
then (P19 /\ Q) <>{} by A63,XBOOLE_1:28;
then P19 meets Q by XBOOLE_0:def 7;
hence not Q is connected by A37,A21,A38,A62,A45,TOPREAL5:1;
the carrier of T =Q by A61,PRE_TOPC:def 5;
then
A74: P199 \/ P299 = the carrier of ((TOP-REAL 2)|P)|Q by A38,XBOOLE_0:def 10;
P299=P29 /\ (the carrier of T) by XBOOLE_1:28;
then
A75: P299 is open by A21,A61,TOPS_2:24;
P199 /\ P299={} by A45,XBOOLE_0:def 7;
hence thesis by A73,A60,A72,A75,A74,Th17;
end;
theorem Th19:
for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2 being
Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & q1 in P & q2 in P holds LE q1,q2,
P,p1,p2 or LE q2,q1,P,p1,p2
proof
let P be non empty Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL 2;
assume that
A1: P is_an_arc_of p1,p2 and
A2: q1 in P and
A3: q2 in P;
per cases;
suppose
q1<>q2;
hence thesis by A1,A2,A3,JORDAN5C:14;
end;
suppose
q1=q2;
hence thesis by A2,JORDAN5C:9;
end;
end;
theorem Th20: :: Another version of TOPMETR3:18
for n being Nat,p1,p2 being Point of TOP-REAL n, P,P1
being non empty Subset of TOP-REAL n st P is_an_arc_of p1,p2 & P1 is_an_arc_of
p1,p2 & P1 c= P holds P1=P
proof
let n be Nat,p1,p2 be Point of TOP-REAL n, P,P1 be non empty
Subset of TOP-REAL n;
assume that
A1: P is_an_arc_of p1,p2 and
A2: P1 is_an_arc_of p1,p2 and
A3: P1 c= P;
P1 is_an_arc_of p2,p1 by A2,JORDAN5B:14;
hence thesis by A1,A3,TOPMETR3:14;
end;
theorem Th21:
for P being non empty Subset of TOP-REAL 2, p1,p2,q1 being Point
of TOP-REAL 2 st P is_an_arc_of p1,p2 & q1 in P & p2<>q1 holds Segment(P,p1,p2,
q1,p2) is_an_arc_of q1,p2
proof
let P be non empty Subset of TOP-REAL 2, p1,p2,q1 be Point of TOP-REAL 2;
assume that
A1: P is_an_arc_of p1,p2 and
A2: q1 in P and
A3: p2<>q1;
LE q1,p2,P,p1,p2 by A1,A2,JORDAN5C:10;
hence thesis by A1,A3,JORDAN16:21;
end;
theorem Th22:
for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,q3 being
Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,
p2 holds Segment(P,p1,p2,q1,q2) \/ Segment(P,p1,p2,q2,q3) =Segment(P,p1,p2,q1,
q3)
proof
let P be non empty Subset of TOP-REAL 2, p1,p2,q1,q2,q3 be Point of TOP-REAL
2;
assume that
A1: P is_an_arc_of p1,p2 and
A2: LE q1,q2,P,p1,p2 and
A3: LE q2,q3,P,p1,p2;
A4: q2 in P by A2,JORDAN5C:def 3;
A5: Segment(P,p1,p2,q1,q3) c= Segment(P,p1,p2,q1,q2) \/ Segment(P,p1,p2,q2, q3)
proof
let x be object;
assume x in Segment(P,p1,p2,q1,q3);
then
x in {p3 where p3 is Point of TOP-REAL 2: LE q1,p3,P,p1,p2 & LE p3,q3
,P,p1,p2} by JORDAN6:26;
then consider p3 being Point of TOP-REAL 2 such that
A6: x=p3 and
A7: LE q1,p3,P,p1,p2 and
A8: LE p3,q3,P,p1,p2;
A9: p3 in P by A7,JORDAN5C:def 3;
now
per cases;
suppose
A10: p3=q2;
then LE p3,q2,P,p1,p2 by A4,JORDAN5C:9;
then x in {p31 where p31 is Point of TOP-REAL 2: LE q1,p31,P,p1,p2 &
LE p31,q2,P,p1,p2} by A2,A6,A10;
hence x in Segment(P,p1,p2,q1,q2) or x in Segment(P,p1,p2,q2,q3) by
JORDAN6:26;
end;
suppose
A11: p3<>q2;
now
per cases by A1,A4,A9,A11,JORDAN5C:14;
case
LE p3,q2,P,p1,p2 & not LE q2,p3,P,p1,p2;
then
x in {p31 where p31 is Point of TOP-REAL 2: LE q1,p31,P,p1,p2
& LE p31,q2,P,p1,p2} by A6,A7;
hence
x in Segment(P,p1,p2,q1,q2) or x in Segment(P,p1,p2,q2,q3) by
JORDAN6:26;
end;
case
LE q2,p3,P,p1,p2 & not LE p3,q2,P,p1,p2;
then
x in {p31 where p31 is Point of TOP-REAL 2: LE q2,p31,P,p1,p2
& LE p31,q3,P,p1,p2} by A6,A8;
hence
x in Segment(P,p1,p2,q1,q2) or x in Segment(P,p1,p2,q2,q3) by
JORDAN6:26;
end;
end;
hence x in Segment(P,p1,p2,q1,q2) or x in Segment(P,p1,p2,q2,q3);
end;
end;
hence thesis by XBOOLE_0:def 3;
end;
Segment(P,p1,p2,q1,q2) \/ Segment(P,p1,p2,q2,q3) c= Segment(P,p1,p2,q1, q3)
proof
let x be object;
assume
A12: x in Segment(P,p1,p2,q1,q2) \/ Segment(P,p1,p2,q2,q3);
per cases by A12,XBOOLE_0:def 3;
suppose
x in Segment(P,p1,p2,q1,q2);
then
x in {p where p is Point of TOP-REAL 2: LE q1,p,P,p1,p2 & LE p,q2,P,
p1,p2} by JORDAN6:26;
then consider p being Point of TOP-REAL 2 such that
A13: x=p & LE q1,p,P,p1,p2 and
A14: LE p,q2,P,p1,p2;
LE p,q3,P,p1,p2 by A3,A14,JORDAN5C:13;
then
x in {p3 where p3 is Point of TOP-REAL 2: LE q1,p3,P,p1,p2 & LE p3,
q3,P,p1,p2} by A13;
hence thesis by JORDAN6:26;
end;
suppose
x in Segment(P,p1,p2,q2,q3);
then
x in {p where p is Point of TOP-REAL 2: LE q2,p,P,p1,p2 & LE p,q3,P
,p1,p2} by JORDAN6:26;
then consider p being Point of TOP-REAL 2 such that
A15: x=p and
A16: LE q2,p,P,p1,p2 and
A17: LE p,q3,P,p1,p2;
LE q1,p,P,p1,p2 by A2,A16,JORDAN5C:13;
then
x in {p3 where p3 is Point of TOP-REAL 2: LE q1,p3,P,p1,p2 & LE p3,
q3,P,p1,p2} by A15,A17;
hence thesis by JORDAN6:26;
end;
end;
hence thesis by A5,XBOOLE_0:def 10;
end;
theorem
for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,q3 being Point
of TOP-REAL 2 st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2
holds Segment(P,p1,p2,q1,q2) /\ Segment(P,p1,p2,q2,q3) = {q2}
proof
let P be non empty Subset of TOP-REAL 2, p1,p2,q1,q2,q3 be Point of TOP-REAL
2;
assume that
A1: P is_an_arc_of p1,p2 and
A2: LE q1,q2,P,p1,p2 and
A3: LE q2,q3,P,p1,p2;
A4: q2 in P by A2,JORDAN5C:def 3;
A5: {q2} c= Segment(P,p1,p2,q1,q2) /\ Segment(P,p1,p2,q2,q3)
proof
set p3=q2;
let x be object;
assume x in {q2};
then
A6: x=q2 by TARSKI:def 1;
LE q2,p3,P,p1,p2 by A4,JORDAN5C:9;
then x in {p31 where p31 is Point of TOP-REAL 2: LE q2,p31,P,p1,p2 & LE
p31,q3,P,p1,p2} by A3,A6;
then
A7: x in Segment(P,p1,p2,q2,q3) by JORDAN6:26;
LE p3,q2,P,p1,p2 by A4,JORDAN5C:9;
then x in {p31 where p31 is Point of TOP-REAL 2: LE q1,p31,P,p1,p2 & LE
p31,q2,P,p1,p2} by A2,A6;
then x in Segment(P,p1,p2,q1,q2) by JORDAN6:26;
hence thesis by A7,XBOOLE_0:def 4;
end;
Segment(P,p1,p2,q1,q2) /\ Segment(P,p1,p2,q2,q3) c= {q2}
proof
let x be object;
assume
A8: x in Segment(P,p1,p2,q1,q2) /\ Segment(P,p1,p2,q2,q3);
then x in Segment(P,p1,p2,q2,q3) by XBOOLE_0:def 4;
then
x in {p4 where p4 is Point of TOP-REAL 2: LE q2,p4,P,p1,p2 & LE p4,q3
,P,p1,p2} by JORDAN6:26;
then
A9: ex p4 being Point of TOP-REAL 2 st x=p4 & LE q2,p4,P,p1, p2 & LE p4,q3
,P,p1,p2;
x in Segment(P,p1,p2,q1,q2) by A8,XBOOLE_0:def 4;
then
x in {p where p is Point of TOP-REAL 2: LE q1,p,P,p1,p2 & LE p,q2,P,p1
,p2} by JORDAN6:26;
then
ex p being Point of TOP-REAL 2 st x=p & LE q1,p,P,p1,p2 & LE p,q2,P,p1 ,p2;
then x=q2 by A1,A9,JORDAN5C:12;
hence thesis by TARSKI:def 1;
end;
hence thesis by A5,XBOOLE_0:def 10;
end;
theorem Th24:
for P being non empty Subset of TOP-REAL 2, p1,p2 being Point of
TOP-REAL 2 st P is_an_arc_of p1,p2 holds Segment(P,p1,p2,p1,p2)=P
proof
let P be non empty Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
assume P is_an_arc_of p1,p2;
then
A1: R_Segment(P,p1,p2,p1)=P & L_Segment(P,p1,p2,p2)=P by JORDAN6:22,24;
R_Segment(P,p1,p2,p1) /\ L_Segment(P,p1,p2,p2)=Segment(P,p1,p2,p1,p2) by
JORDAN6:def 5;
hence thesis by A1;
end;
theorem Th25:
for P,Q1 being non empty Subset of TOP-REAL 2, p1,p2,q1,q2 being
Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & Q1 is_an_arc_of q1,q2 & LE q1,q2,
P,p1,p2 & Q1 c= P holds Q1= Segment(P,p1,p2,q1,q2)
proof
let P,Q1 be non empty Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL
2;
assume that
A1: P is_an_arc_of p1,p2 and
A2: Q1 is_an_arc_of q1,q2 and
A3: LE q1,q2,P,p1,p2 and
A4: Q1 c= P;
reconsider Q0=Segment(P,p1,p2,q1,q2) as non empty Subset of TOP-REAL 2 by A3,
JORDAN16:18;
A5: q1<>q2 by A2,JORDAN6:37;
then
A6: Segment(P,p1,p2,q1,q2) is_an_arc_of q1,q2 by A1,A3,JORDAN16:21;
A7: q2 in P by A3,JORDAN5C:def 3;
A8: now
assume
A9: q1=p2;
LE q2,p2,P,p1,p2 by A1,A7,JORDAN5C:10;
hence contradiction by A1,A2,A3,A9,JORDAN5C:12,JORDAN6:37;
end;
A10: q1 in P by A3,JORDAN5C:def 3;
A11: now
assume
A12: q2=p1;
LE p1,q1,P,p1,p2 by A1,A10,JORDAN5C:10;
hence contradiction by A1,A2,A3,A12,JORDAN5C:12,JORDAN6:37;
end;
A13: p1 in P & p2 in P by A1,TOPREAL1:1;
now
A14: LE p1,q1,P,p1,p2 by A1,A10,JORDAN5C:10;
then
A15: Segment(P,p1,p2,p1,q1)\/ Segment(P,p1,p2,q1,q2) =Segment(P,p1,p2,p1,
q2) by A1,A3,Th22;
A16: [#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 5;
A17: LE q2,p2,P,p1,p2 by A1,A7,JORDAN5C:10;
A18: [#]I[01]=the carrier of I[01];
Q0 is_an_arc_of q1,q2 by A1,A3,A5,JORDAN16:21;
then
A19: q2 in Q0 by TOPREAL1:1;
assume not Q1 c= Q0;
then consider x8 being object such that
A20: x8 in Q1 and
A21: not x8 in Q0;
reconsider q=x8 as Point of TOP-REAL 2 by A20;
A22: q<>q1 by A3,A21,JORDAN16:5;
LE p1,q2,P,p1,p2 by A3,A14,JORDAN5C:13;
then
Segment(P,p1,p2,p1,q2)\/Segment(P,p1,p2,q2,p2)=Segment(P,p1,p2,p1,p2
) by A1,A17,Th22
.=P by A1,Th24;
then
A23: q in Segment(P,p1,p2,p1,q2) or q in Segment(P,p1,p2,q2,p2) by A4,A20,
XBOOLE_0:def 3;
now
per cases by A21,A15,A23,XBOOLE_0:def 3;
case
A24: q in Segment(P,p1,p2,p1,q1);
A25: not q in {q1} by A22,TARSKI:def 1;
not q2 in {q1} by A5,TARSKI:def 1;
then reconsider
Qa=P\{q1} as non empty Subset of (TOP-REAL 2)|P by A7,A16,
XBOOLE_0:def 5,XBOOLE_1:36;
A26: the carrier of ((TOP-REAL 2)|P)|Qa=Qa by PRE_TOPC:8;
reconsider Qa9=Qa as Subset of TOP-REAL 2;
A27: the carrier of ((TOP-REAL 2)|P)|Qa=Qa by PRE_TOPC:8;
A28: Segment(Q1,q1,q2,q,q2) is_an_arc_of q,q2 by A2,A20,A21,A19,Th21;
then consider
f2 being Function of I[01],(TOP-REAL 2)|Segment(Q1,q1,q2,q,q2
) such that
A29: f2 is being_homeomorphism and
A30: f2.0=q & f2.1=q2 by TOPREAL1:def 1;
A31: rng f2=[#]((TOP-REAL 2)|Segment(Q1,q1,q2,q,q2)) by A29,TOPS_2:def 5
.=Segment(Q1,q1,q2,q,q2) by PRE_TOPC:def 5;
A32: ( not p2 in {q1})& not q2 in {q1} by A5,A8,TARSKI:def 1;
q in {p3 where p3 is Point of TOP-REAL 2: LE p1,p3,P,p1,p2 & LE
p3,q1,P,p1,p2} by A24,JORDAN6:26;
then
A33: ex p3 being Point of TOP-REAL 2 st q=p3 & LE p1,p3,P,p1, p2 & LE
p3,q1,P,p1,p2;
A34: now
assume
A35: p1=q1;
then q=p1 by A1,A33,JORDAN5C:12;
hence contradiction by A6,A21,A35,TOPREAL1:1;
end;
then not p1 in {q1} by TARSKI:def 1;
then reconsider
p19=p1,q9=q,q29=q2,p29=p2 as Point of ((TOP-REAL 2)|P)|Qa
by A4,A7,A13,A20,A26,A32,A25,XBOOLE_0:def 5;
now
per cases;
case
q<>p1;
then
A36: Segment(P,p1,p2,p1,q) is_an_arc_of p1,q by A1,A4,A20,JORDAN16:24;
then consider
f1 being Function of I[01],(TOP-REAL 2)|Segment(P,p1,p2,
p1,q) such that
A37: f1 is being_homeomorphism and
A38: f1.0=p1 & f1.1=q by TOPREAL1:def 1;
A39: rng f1=[#]((TOP-REAL 2)|Segment(P,p1,p2,p1,q)) by A37,TOPS_2:def 5
.=Segment(P,p1,p2,p1,q) by PRE_TOPC:def 5;
{p where p is Point of TOP-REAL 2: LE p1,p,P,p1,p2 & LE p,q,P
,p1, p2 } c= Qa
proof
let x be object;
assume x in {p where p is Point of TOP-REAL 2: LE p1,p,P,p1,p2
& LE p,q,P,p1,p2};
then
A40: ex p being Point of TOP-REAL 2 st x=p & LE p1,p,P,p1,p2 & LE
p,q,P,p1,p2;
then x<>q1 by A1,A22,A33,JORDAN5C:12;
then
A41: not x in {q1} by TARSKI:def 1;
x in P by A40,JORDAN5C:def 3;
hence thesis by A41,XBOOLE_0:def 5;
end;
then
A42: Segment(P,p1,p2,p1,q) c= Qa by JORDAN6:26;
dom f1=the carrier of I[01] by A18,A37,TOPS_2:def 5;
then reconsider
g1=f1 as Function of I[01],((TOP-REAL 2)|P)|Qa by A26,A39,A42,
FUNCT_2:2;
A43: f1 is continuous by A37,TOPS_2:def 5;
A44: for G being Subset of ((TOP-REAL 2)|P)|Qa st G is open holds
g1"G is open
proof
let G be Subset of ((TOP-REAL 2)|P)|Qa;
A45: ((TOP-REAL 2)|P)|Qa=(TOP-REAL 2)|Qa9 by PRE_TOPC:7,XBOOLE_1:36;
assume G is open;
then consider G4 being Subset of (TOP-REAL 2) such that
A46: G4 is open and
A47: G=G4 /\ [#]((TOP-REAL 2)|Qa9) by A45,TOPS_2:24;
reconsider G5=G4 /\ [#]((TOP-REAL 2)|Segment(P,p1,p2,p1,q)) as
Subset of ((TOP-REAL 2)|Segment(P,p1,p2,p1,q));
A48: G5 is open by A46,TOPS_2:24;
A49: rng g1=[#]((TOP-REAL 2)|Segment(P,p1,p2,p1,q)) by A37,
TOPS_2:def 5
.= Segment(P,p1,p2,p1,q) by PRE_TOPC:def 5;
A50: p1 in Segment(P,p1,p2,p1,q) by A36,TOPREAL1:1;
A51: f1"G5=g1"(G4 /\ Segment(P,p1,p2,p1,q)) by PRE_TOPC:def 5
.=g1"(G4) /\ g1"(Segment(P,p1,p2,p1,q)) by FUNCT_1:68;
g1"G=g1"G4 /\ g1"([#]((TOP-REAL 2)|Qa9)) by A47,FUNCT_1:68
.=g1"G4 /\ g1"Qa9 by PRE_TOPC:def 5
.=g1"G4 /\ g1"((rng g1) /\ Qa9) by RELAT_1:133
.=g1"G4 /\ g1"(Segment(P,p1,p2,p1,q)) by A42,A49,XBOOLE_1:28;
hence thesis by A43,A50,A48,A51,TOPS_2:43;
end;
[#](((TOP-REAL 2)|P)|Qa) <> {};
then
A52: g1 is continuous by A44,TOPS_2:43;
then p19,q9 are_connected by A38,BORSUK_2:def 1;
then g1 is Path of p19,q9 by A38,A52,BORSUK_2:def 2;
hence ex G1 being Path of p19,q9 st G1 is continuous & G1.0=p19 &
G1.1=q9 by A38,A52;
end;
case
A53: q=p1;
consider g01 being Function of I[01],(((TOP-REAL 2)|P)|Qa) such
that
A54: g01 is continuous & g01.0=p19 & g01.1=p19 by BORSUK_2:3;
p19,p19 are_connected;
then g01 is Path of p19,p19 by A54,BORSUK_2:def 2;
hence ex G1 being Path of p19,q9 st G1 is continuous & G1.0=p19 &
G1.1=q9 by A53,A54;
end;
end;
then consider G1 being Path of p19,q9 such that
A55: G1 is continuous & G1.0=p19 & G1.1=q9;
now
per cases;
case
q2<>p2;
then
A56: Segment(P,p1,p2,q2,p2) is_an_arc_of q2,p2 by A1,A7,Th21;
then consider
f3 being Function of I[01],(TOP-REAL 2)|Segment(P,p1,p2,
q2,p2) such that
A57: f3 is being_homeomorphism and
A58: f3.0=q2 & f3.1=p2 by TOPREAL1:def 1;
A59: rng f3=[#]((TOP-REAL 2)|Segment(P,p1,p2,q2,p2)) by A57,TOPS_2:def 5
.=Segment(P,p1,p2,q2,p2) by PRE_TOPC:def 5;
{p where p is Point of TOP-REAL 2: LE q2,p,P,p1,p2 & LE p,p2
,P,p1, p2} c= Qa
proof
let x be object;
assume x in {p where p is Point of TOP-REAL 2: LE q2,p,P,p1,
p2 & LE p,p2,P,p1,p2};
then
A60: ex p being Point of TOP-REAL 2 st x=p & LE q2,p,P,p1,p2 &
LE p,p2,P,p1,p2;
then x<>q1 by A1,A2,A3,JORDAN5C:12,JORDAN6:37;
then
A61: not x in {q1} by TARSKI:def 1;
x in P by A60,JORDAN5C:def 3;
hence thesis by A61,XBOOLE_0:def 5;
end;
then
A62: Segment(P,p1,p2,q2,p2) c= Qa by JORDAN6:26;
A63: the carrier of ((TOP-REAL 2)|P)|Qa=Qa by PRE_TOPC:8;
dom f3=the carrier of I[01] by A18,A57,TOPS_2:def 5;
then reconsider g3=f3 as Function of I[01],((TOP-REAL 2)|P)|Qa by
A59,A63,A62,FUNCT_2:2;
A64: f3 is continuous by A57,TOPS_2:def 5;
A65: for G being Subset of ((TOP-REAL 2)|P)|Qa st G is open holds
g3"G is open
proof
let G be Subset of ((TOP-REAL 2)|P)|Qa;
A66: ((TOP-REAL 2)|P)|Qa=(TOP-REAL 2)|Qa9 by PRE_TOPC:7,XBOOLE_1:36;
assume G is open;
then consider G4 being Subset of (TOP-REAL 2) such that
A67: G4 is open and
A68: G=G4 /\ [#]((TOP-REAL 2)|Qa9) by A66,TOPS_2:24;
reconsider G5=G4 /\ [#]((TOP-REAL 2)|Segment(P,p1,p2,q2,p2)) as
Subset of ((TOP-REAL 2)|Segment(P,p1,p2,q2,p2));
A69: G5 is open by A67,TOPS_2:24;
A70: rng g3=[#]((TOP-REAL 2)|Segment(P,p1,p2,q2,p2)) by A57,
TOPS_2:def 5
.= Segment(P,p1,p2,q2,p2) by PRE_TOPC:def 5;
A71: p2 in Segment(P,p1,p2,q2,p2) by A56,TOPREAL1:1;
A72: f3"G5=g3"(G4 /\ Segment(P,p1,p2,q2,p2)) by PRE_TOPC:def 5
.=g3"(G4) /\ g3"(Segment(P,p1,p2,q2,p2)) by FUNCT_1:68;
g3"G=g3"G4 /\ g3"([#]((TOP-REAL 2)|Qa9)) by A68,FUNCT_1:68
.=g3"G4 /\ g3"Qa9 by PRE_TOPC:def 5
.=g3"G4 /\ g3"((rng g3) /\ Qa9) by RELAT_1:133
.=g3"G4 /\ g3"(Segment(P,p1,p2,q2,p2)) by A62,A70,XBOOLE_1:28;
hence thesis by A64,A71,A69,A72,TOPS_2:43;
end;
[#](((TOP-REAL 2)|P)|Qa) <> {};
then
A73: g3 is continuous by A65,TOPS_2:43;
then q29,p29 are_connected by A58,BORSUK_2:def 1;
then g3 is Path of q29,p29 by A58,A73,BORSUK_2:def 2;
hence ex G3 being Path of q29,p29 st G3 is continuous & G3.0=q29 &
G3.1=p29 by A58,A73;
end;
case
A74: q2=p2;
consider g01 being Function of I[01],(((TOP-REAL 2)|P)|Qa) such
that
A75: g01 is continuous & g01.0=q29 & g01.1=q29 by BORSUK_2:3;
q29,q29 are_connected;
then g01 is Path of q29,q29 by A75,BORSUK_2:def 2;
hence ex G3 being Path of q29,p29 st G3 is continuous & G3.0=q29 &
G3.1=p29 by A74,A75;
end;
end;
then consider G3 being Path of q29,p29 such that
A76: G3 is continuous & G3.0=q29 & G3.1=p29;
{p where p is Point of TOP-REAL 2: LE q,p,Q1,q1,q2 & LE p,q2,Q1,
q1, q2} c= Qa
proof
let x be object;
assume x in {p where p is Point of TOP-REAL 2: LE q,p,Q1,q1,q2 &
LE p,q2,Q1,q1,q2};
then
A77: ex p being Point of TOP-REAL 2 st x=p & LE q,p,Q1,q1,q2 & LE p,
q2,Q1,q1,q2;
now
assume
A78: x=q1;
LE q1,q,Q1,q1,q2 by A2,A20,JORDAN5C:10;
hence contradiction by A2,A22,A77,A78,JORDAN5C:12;
end;
then
A79: not x in {q1} by TARSKI:def 1;
x in Q1 by A77,JORDAN5C:def 3;
hence thesis by A4,A79,XBOOLE_0:def 5;
end;
then
A80: Segment(Q1,q1,q2,q,q2) c= Qa by JORDAN6:26;
dom f2=the carrier of I[01] by A18,A29,TOPS_2:def 5;
then reconsider g2=f2 as Function of I[01],((TOP-REAL 2)|P)|Qa by A31
,A27,A80,FUNCT_2:2;
A81: f2 is continuous by A29,TOPS_2:def 5;
A82: for G being Subset of ((TOP-REAL 2)|P)|Qa st G is open holds g2"G
is open
proof
let G be Subset of ((TOP-REAL 2)|P)|Qa;
A83: ((TOP-REAL 2)|P)|Qa=(TOP-REAL 2)|Qa9 by PRE_TOPC:7,XBOOLE_1:36;
assume G is open;
then consider G4 being Subset of (TOP-REAL 2) such that
A84: G4 is open and
A85: G=G4 /\ [#]((TOP-REAL 2)|Qa9) by A83,TOPS_2:24;
reconsider G5=G4 /\ [#]((TOP-REAL 2)|Segment(Q1,q1,q2,q,q2)) as
Subset of ((TOP-REAL 2)|Segment(Q1,q1,q2,q,q2));
A86: G5 is open by A84,TOPS_2:24;
A87: rng g2=[#]((TOP-REAL 2)|Segment(Q1,q1,q2,q,q2)) by A29,TOPS_2:def 5
.= Segment(Q1,q1,q2,q,q2) by PRE_TOPC:def 5;
A88: q2 in Segment(Q1,q1,q2,q,q2) by A28,TOPREAL1:1;
A89: f2"G5=g2"(G4 /\ Segment(Q1,q1,q2,q,q2)) by PRE_TOPC:def 5
.=g2"(G4) /\ g2"(Segment(Q1,q1,q2,q,q2)) by FUNCT_1:68;
g2"G=g2"G4 /\ g2"([#]((TOP-REAL 2)|Qa9)) by A85,FUNCT_1:68
.=g2"G4 /\ g2"Qa9 by PRE_TOPC:def 5
.=g2"G4 /\ g2"((rng g2) /\ Qa9) by RELAT_1:133
.=g2"G4 /\ g2"(Segment(Q1,q1,q2,q,q2)) by A80,A87,XBOOLE_1:28;
hence thesis by A81,A88,A86,A89,TOPS_2:43;
end;
[#](((TOP-REAL 2)|P)|Qa) <> {};
then
A90: g2 is continuous by A82,TOPS_2:43;
then q9,q29 are_connected by A30,BORSUK_2:def 1;
then reconsider G2=g2 as Path of q9,q29 by A30,A90,BORSUK_2:def 2;
A91: (G1+G2).1=q29 by A55,A30,A90,BORSUK_2:14;
A92: (G1+G2) is continuous & (G1+G2).0=p19 by A55,A30,A90,BORSUK_2:14;
then
A93: ((G1+G2)+G3).1=p29 by A91,A76,BORSUK_2:14;
(G1+G2)+G3 is continuous & ((G1+G2)+G3).0=p19 by A92,A91,A76,
BORSUK_2:14;
hence contradiction by A1,A10,A8,A34,A93,Th18;
end;
case
A94: q in Segment(P,p1,p2,q2,p2);
A95: ( not p1 in {q2})& not q1 in {q2} by A5,A11,TARSKI:def 1;
not q1 in {q2} by A5,TARSKI:def 1;
then reconsider
Qa=P\{q2} as non empty Subset of (TOP-REAL 2)|P by A10,A16,
XBOOLE_0:def 5,XBOOLE_1:36;
A96: the carrier of ((TOP-REAL 2)|P)|Qa=Qa by PRE_TOPC:8;
reconsider Qa9=Qa as Subset of TOP-REAL 2;
A97: the carrier of ((TOP-REAL 2)|P)|Qa=Qa by PRE_TOPC:8;
A98: Segment(Q1,q1,q2,q1,q) is_an_arc_of q1,q by A2,A20,A22,JORDAN16:24;
then consider
f2 being Function of I[01],(TOP-REAL 2)|Segment(Q1,q1,q2,q1,q
) such that
A99: f2 is being_homeomorphism and
A100: f2.0=q1 & f2.1=q by TOPREAL1:def 1;
A101: rng f2=[#]((TOP-REAL 2)|Segment(Q1,q1,q2,q1,q)) by A99,TOPS_2:def 5
.=Segment(Q1,q1,q2,q1,q) by PRE_TOPC:def 5;
A102: not q in {q2} by A21,A19,TARSKI:def 1;
q in {p3 where p3 is Point of TOP-REAL 2: LE q2,p3,P,p1,p2 & LE
p3,p2,P,p1,p2} by A94,JORDAN6:26;
then
A103: ex p3 being Point of TOP-REAL 2 st q=p3 & LE q2,p3,P,p1, p2 & LE
p3,p2,P,p1,p2;
A104: now
assume
A105: p2=q2;
then q=p2 by A1,A103,JORDAN5C:12;
hence contradiction by A6,A21,A105,TOPREAL1:1;
end;
then not p2 in {q2} by TARSKI:def 1;
then reconsider
p19=p1,q9=q,q19=q1,p29=p2 as Point of ((TOP-REAL 2)|P)|Qa
by A4,A10,A13,A20,A96,A95,A102,XBOOLE_0:def 5;
now
per cases;
case
q<>p2;
then
A106: Segment(P,p1,p2,q,p2) is_an_arc_of q,p2 by A1,A4,A20,Th21;
then consider
f1 being Function of I[01],(TOP-REAL 2)|Segment(P,p1,p2,q
,p2) such that
A107: f1 is being_homeomorphism and
A108: f1.0=q & f1.1=p2 by TOPREAL1:def 1;
A109: rng f1=[#]((TOP-REAL 2)|Segment(P,p1,p2,q,p2)) by A107,TOPS_2:def 5
.=Segment(P,p1,p2,q,p2) by PRE_TOPC:def 5;
{p where p is Point of TOP-REAL 2: LE q,p,P,p1,p2 & LE p,p2,
P,p1, p2} c= Qa
proof
let x be object;
assume x in {p where p is Point of TOP-REAL 2: LE q,p,P,p1,p2
& LE p,p2,P,p1,p2};
then
A110: ex p being Point of TOP-REAL 2 st x=p & LE q,p,P,p1,p2 & LE
p,p2,P,p1,p2;
then x<>q2 by A1,A21,A19,A103,JORDAN5C:12;
then
A111: not x in {q2} by TARSKI:def 1;
x in P by A110,JORDAN5C:def 3;
hence thesis by A111,XBOOLE_0:def 5;
end;
then
A112: Segment(P,p1,p2,q,p2) c= Qa by JORDAN6:26;
dom f1=the carrier of I[01] by A18,A107,TOPS_2:def 5;
then reconsider
g1=f1 as Function of I[01],((TOP-REAL 2)|P)|Qa by A96,A109,A112,
FUNCT_2:2;
A113: f1 is continuous by A107,TOPS_2:def 5;
A114: for G being Subset of ((TOP-REAL 2)|P)|Qa st G is open holds
g1"G is open
proof
let G be Subset of ((TOP-REAL 2)|P)|Qa;
A115: ((TOP-REAL 2)|P)|Qa=(TOP-REAL 2)|Qa9 by PRE_TOPC:7,XBOOLE_1:36;
assume G is open;
then consider G4 being Subset of (TOP-REAL 2) such that
A116: G4 is open and
A117: G=G4 /\ [#]((TOP-REAL 2)|Qa9) by A115,TOPS_2:24;
reconsider G5=G4 /\ [#]((TOP-REAL 2)|Segment(P,p1,p2,q,p2)) as
Subset of ((TOP-REAL 2)|Segment(P,p1,p2,q,p2));
A118: G5 is open by A116,TOPS_2:24;
A119: rng g1=[#]((TOP-REAL 2)|Segment(P,p1,p2,q,p2)) by A107,
TOPS_2:def 5
.= Segment(P,p1,p2,q,p2) by PRE_TOPC:def 5;
A120: p2 in Segment(P,p1,p2,q,p2) by A106,TOPREAL1:1;
A121: f1"G5=g1"(G4 /\ Segment(P,p1,p2,q,p2)) by PRE_TOPC:def 5
.=g1"(G4) /\ g1"(Segment(P,p1,p2,q,p2)) by FUNCT_1:68;
g1"G=g1"G4 /\ g1"([#]((TOP-REAL 2)|Qa9)) by A117,FUNCT_1:68
.=g1"G4 /\ g1"Qa9 by PRE_TOPC:def 5
.=g1"G4 /\ g1"((rng g1) /\ Qa9) by RELAT_1:133
.=g1"G4 /\ g1"(Segment(P,p1,p2,q,p2)) by A112,A119,XBOOLE_1:28;
hence thesis by A113,A120,A118,A121,TOPS_2:43;
end;
[#](((TOP-REAL 2)|P)|Qa) <> {};
then
A122: g1 is continuous by A114,TOPS_2:43;
then q9,p29 are_connected by A108,BORSUK_2:def 1;
then g1 is Path of q9,p29 by A108,A122,BORSUK_2:def 2;
hence
ex G1 being Path of q9,p29 st G1 is continuous & G1.0=q9 & G1
.1=p29 by A108,A122;
end;
case
A123: q=p2;
consider g01 being Function of I[01],(((TOP-REAL 2)|P)|Qa) such
that
A124: g01 is continuous & g01.0=p29 & g01.1=p29 by BORSUK_2:3;
p29,p29 are_connected;
then g01 is Path of p29,p29 by A124,BORSUK_2:def 2;
hence
ex G1 being Path of q9,p29 st G1 is continuous & G1.0=q9 & G1
.1=p29 by A123,A124;
end;
end;
then consider G1 being Path of q9,p29 such that
A125: G1 is continuous & G1.0=q9 & G1.1=p29;
now
per cases;
case
q1<>p1;
then
A126: Segment(P,p1,p2,p1,q1) is_an_arc_of p1,q1 by A1,A10,JORDAN16:24;
then consider
f3 being Function of I[01],(TOP-REAL 2)|Segment(P,p1,p2,
p1,q1) such that
A127: f3 is being_homeomorphism and
A128: f3.0=p1 & f3.1=q1 by TOPREAL1:def 1;
A129: rng f3=[#]((TOP-REAL 2)|Segment(P,p1,p2,p1,q1)) by A127,
TOPS_2:def 5
.=Segment(P,p1,p2,p1,q1) by PRE_TOPC:def 5;
{p where p is Point of TOP-REAL 2: LE p1,p,P,p1,p2 & LE p,q1
,P,p1, p2} c= Qa
proof
let x be object;
assume x in {p where p is Point of TOP-REAL 2: LE p1,p,P,p1,
p2 & LE p,q1,P,p1,p2};
then
A130: ex p being Point of TOP-REAL 2 st x=p & LE p1,p,P,p1,p2 &
LE p,q1,P,p1,p2;
then x<>q2 by A1,A2,A3,JORDAN5C:12,JORDAN6:37;
then
A131: not x in {q2} by TARSKI:def 1;
x in P by A130,JORDAN5C:def 3;
hence thesis by A131,XBOOLE_0:def 5;
end;
then
A132: Segment(P,p1,p2,p1,q1) c= Qa by JORDAN6:26;
A133: the carrier of ((TOP-REAL 2)|P)|Qa=Qa by PRE_TOPC:8;
dom f3=the carrier of I[01] by A18,A127,TOPS_2:def 5;
then reconsider g3=f3 as Function of I[01],((TOP-REAL 2)|P)|Qa by
A129,A133,A132,FUNCT_2:2;
A134: f3 is continuous by A127,TOPS_2:def 5;
A135: for G being Subset of ((TOP-REAL 2)|P)|Qa st G is open holds
g3"G is open
proof
let G be Subset of ((TOP-REAL 2)|P)|Qa;
A136: ((TOP-REAL 2)|P)|Qa=(TOP-REAL 2)|Qa9 by PRE_TOPC:7,XBOOLE_1:36;
assume G is open;
then consider G4 being Subset of (TOP-REAL 2) such that
A137: G4 is open and
A138: G=G4 /\ [#]((TOP-REAL 2)|Qa9) by A136,TOPS_2:24;
reconsider G5=G4 /\ [#]((TOP-REAL 2)|Segment(P,p1,p2,p1,q1)) as
Subset of ((TOP-REAL 2)|Segment(P,p1,p2,p1,q1));
A139: G5 is open by A137,TOPS_2:24;
A140: rng g3=[#]((TOP-REAL 2)|Segment(P,p1,p2,p1,q1)) by A127,
TOPS_2:def 5
.= Segment(P,p1,p2,p1,q1) by PRE_TOPC:def 5;
A141: p1 in Segment(P,p1,p2,p1,q1) by A126,TOPREAL1:1;
A142: f3"G5=g3"(G4 /\ Segment(P,p1,p2,p1,q1)) by PRE_TOPC:def 5
.=g3"(G4) /\ g3"(Segment(P,p1,p2,p1,q1)) by FUNCT_1:68;
g3"G=g3"G4 /\ g3"([#]((TOP-REAL 2)|Qa9)) by A138,FUNCT_1:68
.=g3"G4 /\ g3"Qa9 by PRE_TOPC:def 5
.=g3"G4 /\ g3"((rng g3) /\ Qa9) by RELAT_1:133
.=g3"G4 /\ g3"(Segment(P,p1,p2,p1,q1)) by A132,A140,XBOOLE_1:28
;
hence thesis by A134,A141,A139,A142,TOPS_2:43;
end;
[#](((TOP-REAL 2)|P)|Qa) <> {};
then
A143: g3 is continuous by A135,TOPS_2:43;
then p19,q19 are_connected by A128,BORSUK_2:def 1;
then g3 is Path of p19,q19 by A128,A143,BORSUK_2:def 2;
hence ex G3 being Path of p19,q19 st G3 is continuous & G3.0=p19 &
G3.1=q19 by A128,A143;
end;
case
A144: q1=p1;
consider g01 being Function of I[01],(((TOP-REAL 2)|P)|Qa) such
that
A145: g01 is continuous & g01.0=q19 & g01.1=q19 by BORSUK_2:3;
q19,q19 are_connected;
then g01 is Path of q19,q19 by A145,BORSUK_2:def 2;
hence ex G3 being Path of p19,q19 st G3 is continuous & G3.0=p19 &
G3.1=q19 by A144,A145;
end;
end;
then consider G3 being Path of p19,q19 such that
A146: G3 is continuous & G3.0=p19 & G3.1=q19;
{p where p is Point of TOP-REAL 2: LE q1,p,Q1,q1,q2 & LE p,q,Q1,
q1,q2} c= Qa
proof
let x be object;
assume x in {p where p is Point of TOP-REAL 2: LE q1,p,Q1,q1,q2 &
LE p,q,Q1,q1,q2};
then
A147: ex p being Point of TOP-REAL 2 st x=p & LE q1,p,Q1,q1,q2 & LE p
,q,Q1,q1,q2;
now
assume
A148: x=q2;
LE q,q2,Q1,q1,q2 by A2,A20,JORDAN5C:10;
hence contradiction by A2,A21,A19,A147,A148,JORDAN5C:12;
end;
then
A149: not x in {q2} by TARSKI:def 1;
x in Q1 by A147,JORDAN5C:def 3;
hence thesis by A4,A149,XBOOLE_0:def 5;
end;
then
A150: Segment(Q1,q1,q2,q1,q) c= Qa by JORDAN6:26;
dom f2=the carrier of I[01] by A18,A99,TOPS_2:def 5;
then reconsider g2=f2 as Function of I[01],((TOP-REAL 2)|P)|Qa by A101
,A97,A150,FUNCT_2:2;
A151: f2 is continuous by A99,TOPS_2:def 5;
A152: for G being Subset of ((TOP-REAL 2)|P)|Qa st G is open holds g2"
G is open
proof
let G be Subset of ((TOP-REAL 2)|P)|Qa;
A153: ((TOP-REAL 2)|P)|Qa=(TOP-REAL 2)|Qa9 by PRE_TOPC:7,XBOOLE_1:36;
assume G is open;
then consider G4 being Subset of (TOP-REAL 2) such that
A154: G4 is open and
A155: G=G4 /\ [#]((TOP-REAL 2)|Qa9) by A153,TOPS_2:24;
reconsider G5=G4 /\ [#]((TOP-REAL 2)|Segment(Q1,q1,q2,q1,q)) as
Subset of ((TOP-REAL 2)|Segment(Q1,q1,q2,q1,q));
A156: G5 is open by A154,TOPS_2:24;
A157: rng g2=[#]((TOP-REAL 2)|Segment(Q1,q1,q2,q1,q)) by A99,TOPS_2:def 5
.= Segment(Q1,q1,q2,q1,q) by PRE_TOPC:def 5;
A158: q1 in Segment(Q1,q1,q2,q1,q) by A98,TOPREAL1:1;
A159: f2"G5=g2"(G4 /\ Segment(Q1,q1,q2,q1,q)) by PRE_TOPC:def 5
.=g2"(G4) /\ g2"(Segment(Q1,q1,q2,q1,q)) by FUNCT_1:68;
g2"G=g2"G4 /\ g2"([#]((TOP-REAL 2)|Qa9)) by A155,FUNCT_1:68
.=g2"G4 /\ g2"Qa9 by PRE_TOPC:def 5
.=g2"G4 /\ g2"((rng g2) /\ Qa9) by RELAT_1:133
.=g2"G4 /\ g2"(Segment(Q1,q1,q2,q1,q)) by A150,A157,XBOOLE_1:28;
hence thesis by A151,A158,A156,A159,TOPS_2:43;
end;
[#](((TOP-REAL 2)|P)|Qa) <> {};
then
A160: g2 is continuous by A152,TOPS_2:43;
then q19,q9 are_connected by A100,BORSUK_2:def 1;
then reconsider G2=g2 as Path of q19,q9 by A100,A160,BORSUK_2:def 2;
A161: (G2+G1).1=p29 by A125,A100,A160,BORSUK_2:14;
A162: (G2+G1) is continuous & (G2+G1).0=q19 by A125,A100,A160,BORSUK_2:14;
then
A163: (G3+(G2+G1)).1=p29 by A161,A146,BORSUK_2:14;
G3+(G2+G1) is continuous & (G3+(G2+G1)).0=p19 by A162,A161,A146,
BORSUK_2:14;
hence contradiction by A1,A7,A11,A104,A163,Th18;
end;
end;
hence contradiction;
end;
hence thesis by A2,A6,Th20;
end;
theorem
for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p being Point
of TOP-REAL 2,e being Real st q1 is_Lin P,p1,p2,e & q2`1=e & LSeg(q1,q2) c= P &
p in LSeg(q1,q2) holds p is_Lin P,p1,p2,e
proof
let P be non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p be Point of TOP-REAL
2,e be Real;
assume that
A1: q1 is_Lin P,p1,p2,e and
A2: q2`1=e and
A3: LSeg(q1,q2) c= P and
A4: p in LSeg(q1,q2);
A5: q1 in P by A1;
A6: q2 in LSeg(q1,q2) by RLTOPSP1:68;
A7: q1`1=e by A1;
consider p4 being Point of TOP-REAL 2 such that
A8: p4`1<e and
A9: LE p4,q1,P,p1,p2 and
A10: for p5 being Point of TOP-REAL 2 st LE p4,p5,P,p1,p2 & LE p5,q1,P,
p1,p2 holds p5`1<=e by A1;
A11: P is_an_arc_of p1,p2 by A1;
A12: p4 in P by A9,JORDAN5C:def 3;
now
per cases by A3,A11,A5,A6,Th19;
case
A13: LE q1,q2,P,p1,p2;
A14: now
per cases;
case
q1<>q2;
then LSeg(q1,q2) is_an_arc_of q1,q2 by TOPREAL1:9;
hence Segment(P,p1,p2,q1,q2) =LSeg(q1,q2) by A3,A11,A13,Th25;
end;
case
A15: q1=q2;
then LSeg(q1,q2)={q1} by RLTOPSP1:70;
hence Segment(P,p1,p2,q1,q2) =LSeg(q1,q2) by A11,A5,A15,Th1;
end;
end;
Segment(P,p1,p2,q1,q2) = {p3 where p3 is Point of TOP-REAL 2: LE q1
,p3,P,p1,p2 & LE p3,q2,P,p1,p2} by JORDAN6:26;
then
A16: ex p3 being Point of TOP-REAL 2 st p=p3 & LE q1,p3,P,p1, p2 & LE p3,
q2,P,p1,p2 by A4,A14;
then
A17: LE p4,p,P,p1,p2 by A9,JORDAN5C:13;
A18: for p6 being Point of TOP-REAL 2 st LE p4,p6,P,p1,p2 & LE p6,p,P,p1
,p2 holds p6`1<=e
proof
let p6 be Point of TOP-REAL 2;
assume that
A19: LE p4,p6,P,p1,p2 and
A20: LE p6,p,P,p1,p2;
A21: p6 in P by A19,JORDAN5C:def 3;
now
per cases by A11,A5,A21,Th19;
case
LE p6,q1,P,p1,p2;
hence thesis by A10,A19;
end;
case
A22: LE q1,p6,P,p1,p2;
LE p6,q2,P,p1,p2 by A16,A20,JORDAN5C:13;
then p6 in {qq where qq is Point of TOP-REAL 2: LE q1,qq,P,p1, p2
& LE qq,q2,P,p1,p2} by A22;
then p6 in LSeg(q1,q2) by A14,JORDAN6:26;
hence thesis by A2,A7,GOBOARD7:5;
end;
end;
hence thesis;
end;
p`1=e by A2,A4,A7,GOBOARD7:5;
hence thesis by A3,A4,A11,A8,A17,A18;
end;
case
A23: LE q2,q1,P,p1,p2;
A24: now
per cases;
case
q1<>q2;
then LSeg(q2,q1) is_an_arc_of q2,q1 by TOPREAL1:9;
hence Segment(P,p1,p2,q2,q1) =LSeg(q2,q1) by A3,A11,A23,Th25;
end;
case
A25: q1=q2;
then LSeg(q2,q1)={q1} by RLTOPSP1:70;
hence Segment(P,p1,p2,q2,q1) =LSeg(q2,q1) by A11,A5,A25,Th1;
end;
end;
A26: now
assume LE q2,p4,P,p1,p2;
then p4 in {qq where qq is Point of TOP-REAL 2: LE q2,qq,P,p1,p2 & LE
qq,q1,P,p1,p2} by A9;
then p4 in Segment(P,p1,p2,q2,q1) by JORDAN6:26;
hence contradiction by A2,A7,A8,A24,GOBOARD7:5;
end;
Segment(P,p1,p2,q2,q1) = {p3 where p3 is Point of TOP-REAL 2: LE q2
,p3,P,p1,p2 & LE p3,q1,P,p1,p2} by JORDAN6:26;
then
A27: ex p3 being Point of TOP-REAL 2 st p=p3 & LE q2,p3,P,p1, p2 & LE p3,
q1,P,p1,p2 by A4,A24;
A28: for p6 being Point of TOP-REAL 2 st LE p4,p6,P,p1,p2 & LE p6,p,P,p1
,p2 holds p6`1<=e
proof
let p6 be Point of TOP-REAL 2;
assume that
A29: LE p4,p6,P,p1,p2 and
A30: LE p6,p,P,p1,p2;
LE p6,q1,P,p1,p2 by A27,A30,JORDAN5C:13;
hence thesis by A10,A29;
end;
LE q2,p4,P,p1,p2 or LE p4,q2,P,p1,p2 by A3,A11,A6,A12,Th19;
then
A31: LE p4,p,P,p1,p2 by A27,A26,JORDAN5C:13;
p`1=e by A2,A4,A7,GOBOARD7:5;
hence thesis by A3,A4,A11,A8,A31,A28;
end;
end;
hence thesis;
end;
theorem
for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p being Point
of TOP-REAL 2,e being Real st q1 is_Rin P,p1,p2,e & q2`1=e & LSeg(q1,q2) c= P &
p in LSeg(q1,q2) holds p is_Rin P,p1,p2,e
proof
let P be non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p be Point of TOP-REAL
2,e be Real;
assume that
A1: q1 is_Rin P,p1,p2,e and
A2: q2`1=e and
A3: LSeg(q1,q2) c= P and
A4: p in LSeg(q1,q2);
A5: q1 in P by A1;
A6: q2 in LSeg(q1,q2) by RLTOPSP1:68;
A7: q1`1=e by A1;
consider p4 being Point of TOP-REAL 2 such that
A8: p4`1>e and
A9: LE p4,q1,P,p1,p2 and
A10: for p5 being Point of TOP-REAL 2 st LE p4,p5,P,p1,p2 & LE p5,q1,P,
p1,p2 holds p5`1>=e by A1;
A11: P is_an_arc_of p1,p2 by A1;
A12: p4 in P by A9,JORDAN5C:def 3;
now
per cases by A3,A11,A5,A6,Th19;
case
A13: LE q1,q2,P,p1,p2;
A14: now
per cases;
case
q1<>q2;
then LSeg(q1,q2) is_an_arc_of q1,q2 by TOPREAL1:9;
hence Segment(P,p1,p2,q1,q2) =LSeg(q1,q2) by A3,A11,A13,Th25;
end;
case
A15: q1=q2;
then LSeg(q1,q2)={q1} by RLTOPSP1:70;
hence Segment(P,p1,p2,q1,q2) =LSeg(q1,q2) by A11,A5,A15,Th1;
end;
end;
Segment(P,p1,p2,q1,q2) = {p3 where p3 is Point of TOP-REAL 2: LE q1
,p3,P,p1,p2 & LE p3,q2,P,p1,p2} by JORDAN6:26;
then
A16: ex p3 being Point of TOP-REAL 2 st p=p3 & LE q1,p3,P,p1, p2 & LE p3,
q2,P,p1,p2 by A4,A14;
then
A17: LE p4,p,P,p1,p2 by A9,JORDAN5C:13;
A18: for p6 being Point of TOP-REAL 2 st LE p4,p6,P,p1,p2 & LE p6,p,P,p1
,p2 holds p6`1>=e
proof
let p6 be Point of TOP-REAL 2;
assume that
A19: LE p4,p6,P,p1,p2 and
A20: LE p6,p,P,p1,p2;
A21: p6 in P by A19,JORDAN5C:def 3;
now
per cases by A11,A5,A21,Th19;
case
LE p6,q1,P,p1,p2;
hence thesis by A10,A19;
end;
case
A22: LE q1,p6,P,p1,p2;
LE p6,q2,P,p1,p2 by A16,A20,JORDAN5C:13;
then p6 in {qq where qq is Point of TOP-REAL 2: LE q1,qq,P,p1, p2
& LE qq,q2,P,p1,p2} by A22;
then p6 in LSeg(q1,q2) by A14,JORDAN6:26;
hence thesis by A2,A7,GOBOARD7:5;
end;
end;
hence thesis;
end;
p`1=e by A2,A4,A7,GOBOARD7:5;
hence thesis by A3,A4,A11,A8,A17,A18;
end;
case
A23: LE q2,q1,P,p1,p2;
A24: now
per cases;
case
q1<>q2;
then LSeg(q2,q1) is_an_arc_of q2,q1 by TOPREAL1:9;
hence Segment(P,p1,p2,q2,q1) =LSeg(q2,q1) by A3,A11,A23,Th25;
end;
case
A25: q1=q2;
then LSeg(q2,q1)={q1} by RLTOPSP1:70;
hence Segment(P,p1,p2,q2,q1) =LSeg(q2,q1) by A11,A5,A25,Th1;
end;
end;
A26: now
assume LE q2,p4,P,p1,p2;
then p4 in {qq where qq is Point of TOP-REAL 2: LE q2,qq,P,p1,p2 & LE
qq,q1,P,p1,p2} by A9;
then p4 in Segment(P,p1,p2,q2,q1) by JORDAN6:26;
hence contradiction by A2,A7,A8,A24,GOBOARD7:5;
end;
Segment(P,p1,p2,q2,q1) = {p3 where p3 is Point of TOP-REAL 2: LE q2
,p3,P,p1,p2 & LE p3,q1,P,p1,p2} by JORDAN6:26;
then
A27: ex p3 being Point of TOP-REAL 2 st p=p3 & LE q2,p3,P,p1, p2 & LE p3,
q1,P,p1,p2 by A4,A24;
A28: for p6 being Point of TOP-REAL 2 st LE p4,p6,P,p1,p2 & LE p6,p,P,p1
,p2 holds p6`1>=e
proof
let p6 be Point of TOP-REAL 2;
assume that
A29: LE p4,p6,P,p1,p2 and
A30: LE p6,p,P,p1,p2;
LE p6,q1,P,p1,p2 by A27,A30,JORDAN5C:13;
hence thesis by A10,A29;
end;
LE q2,p4,P,p1,p2 or LE p4,q2,P,p1,p2 by A3,A11,A6,A12,Th19;
then
A31: LE p4,p,P,p1,p2 by A27,A26,JORDAN5C:13;
p`1=e by A2,A4,A7,GOBOARD7:5;
hence thesis by A3,A4,A11,A8,A31,A28;
end;
end;
hence thesis;
end;
theorem
for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p being Point
of TOP-REAL 2,e being Real st q1 is_Lout P,p1,p2,e & q2`1=e & LSeg(q1,q2) c= P
& p in LSeg(q1,q2) holds p is_Lout P,p1,p2,e
proof
let P be non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p be Point of TOP-REAL
2,e be Real;
assume that
A1: q1 is_Lout P,p1,p2,e and
A2: q2`1=e and
A3: LSeg(q1,q2) c= P and
A4: p in LSeg(q1,q2);
A5: q1 in P by A1;
A6: q2 in LSeg(q1,q2) by RLTOPSP1:68;
A7: q1`1=e by A1;
consider p4 being Point of TOP-REAL 2 such that
A8: p4`1<e and
A9: LE q1,p4,P,p1,p2 and
A10: for p5 being Point of TOP-REAL 2 st LE p5,p4,P,p1,p2 & LE q1,p5,P,
p1,p2 holds p5`1<=e by A1;
A11: P is_an_arc_of p1,p2 by A1;
A12: p4 in P by A9,JORDAN5C:def 3;
now
per cases by A3,A11,A5,A6,Th19;
case
A13: LE q2,q1,P,p1,p2;
A14: now
per cases;
case
q1<>q2;
then LSeg(q2,q1) is_an_arc_of q2,q1 by TOPREAL1:9;
hence Segment(P,p1,p2,q2,q1) =LSeg(q2,q1) by A3,A11,A13,Th25;
end;
case
A15: q1=q2;
then LSeg(q1,q2)={q1} by RLTOPSP1:70;
hence Segment(P,p1,p2,q2,q1) =LSeg(q2,q1) by A11,A5,A15,Th1;
end;
end;
Segment(P,p1,p2,q2,q1) = {p3 where p3 is Point of TOP-REAL 2: LE q2
,p3,P,p1,p2 & LE p3,q1,P,p1,p2} by JORDAN6:26;
then
A16: ex p3 being Point of TOP-REAL 2 st p=p3 & LE q2,p3,P,p1, p2 & LE p3,
q1,P,p1,p2 by A4,A14;
then
A17: LE p,p4,P,p1,p2 by A9,JORDAN5C:13;
A18: for p6 being Point of TOP-REAL 2 st LE p6,p4,P,p1,p2 & LE p,p6,P,p1
,p2 holds p6`1<=e
proof
let p6 be Point of TOP-REAL 2;
assume that
A19: LE p6,p4,P,p1,p2 and
A20: LE p,p6,P,p1,p2;
A21: p6 in P by A19,JORDAN5C:def 3;
now
per cases by A11,A5,A21,Th19;
case
LE q1,p6,P,p1,p2;
hence thesis by A10,A19;
end;
case
A22: LE p6,q1,P,p1,p2;
LE q2,p6,P,p1,p2 by A16,A20,JORDAN5C:13;
then p6 in {qq where qq is Point of TOP-REAL 2: LE q2,qq,P,p1, p2
& LE qq,q1,P,p1,p2} by A22;
then p6 in LSeg(q2,q1) by A14,JORDAN6:26;
hence thesis by A2,A7,GOBOARD7:5;
end;
end;
hence thesis;
end;
p`1=e by A2,A4,A7,GOBOARD7:5;
hence thesis by A3,A4,A11,A8,A17,A18;
end;
case
A23: LE q1,q2,P,p1,p2;
A24: now
per cases;
case
q1<>q2;
then LSeg(q1,q2) is_an_arc_of q1,q2 by TOPREAL1:9;
hence Segment(P,p1,p2,q1,q2) =LSeg(q1,q2) by A3,A11,A23,Th25;
end;
case
A25: q1=q2;
then LSeg(q2,q1)={q1} by RLTOPSP1:70;
hence Segment(P,p1,p2,q1,q2) =LSeg(q1,q2) by A11,A5,A25,Th1;
end;
end;
A26: now
assume LE p4,q2,P,p1,p2;
then p4 in {qq where qq is Point of TOP-REAL 2: LE q1,qq,P,p1,p2 & LE
qq,q2,P,p1,p2} by A9;
then p4 in Segment(P,p1,p2,q1,q2) by JORDAN6:26;
hence contradiction by A2,A7,A8,A24,GOBOARD7:5;
end;
Segment(P,p1,p2,q1,q2) = {p3 where p3 is Point of TOP-REAL 2: LE q1
,p3,P,p1,p2 & LE p3,q2,P,p1,p2} by JORDAN6:26;
then
A27: ex p3 being Point of TOP-REAL 2 st p=p3 & LE q1,p3,P,p1, p2 & LE p3,
q2,P,p1,p2 by A4,A24;
A28: for p6 being Point of TOP-REAL 2 st LE p6,p4,P,p1,p2 & LE p,p6,P,p1
,p2 holds p6`1<=e
proof
let p6 be Point of TOP-REAL 2;
assume that
A29: LE p6,p4,P,p1,p2 and
A30: LE p,p6,P,p1,p2;
LE q1,p6,P,p1,p2 by A27,A30,JORDAN5C:13;
hence thesis by A10,A29;
end;
LE q2,p4,P,p1,p2 or LE p4,q2,P,p1,p2 by A3,A11,A6,A12,Th19;
then
A31: LE p,p4,P,p1,p2 by A27,A26,JORDAN5C:13;
p`1=e by A2,A4,A7,GOBOARD7:5;
hence thesis by A3,A4,A11,A8,A31,A28;
end;
end;
hence thesis;
end;
theorem
for P being non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p being Point
of TOP-REAL 2,e being Real st q1 is_Rout P,p1,p2,e & q2`1=e & LSeg(q1,q2) c= P
& p in LSeg(q1,q2) holds p is_Rout P,p1,p2,e
proof
let P be non empty Subset of TOP-REAL 2, p1,p2,q1,q2,p be Point of TOP-REAL
2,e be Real;
assume that
A1: q1 is_Rout P,p1,p2,e and
A2: q2`1=e and
A3: LSeg(q1,q2) c= P and
A4: p in LSeg(q1,q2);
A5: q1 in P by A1;
A6: q2 in LSeg(q1,q2) by RLTOPSP1:68;
A7: q1`1=e by A1;
consider p4 being Point of TOP-REAL 2 such that
A8: p4`1>e and
A9: LE q1,p4,P,p1,p2 and
A10: for p5 being Point of TOP-REAL 2 st LE p5,p4,P,p1,p2 & LE q1,p5,P,
p1,p2 holds p5`1>=e by A1;
A11: P is_an_arc_of p1,p2 by A1;
A12: p4 in P by A9,JORDAN5C:def 3;
now
per cases by A3,A11,A5,A6,Th19;
case
A13: LE q2,q1,P,p1,p2;
A14: now
per cases;
case
q1<>q2;
then LSeg(q2,q1) is_an_arc_of q2,q1 by TOPREAL1:9;
hence Segment(P,p1,p2,q2,q1) =LSeg(q2,q1) by A3,A11,A13,Th25;
end;
case
A15: q1=q2;
then LSeg(q1,q2)={q1} by RLTOPSP1:70;
hence Segment(P,p1,p2,q2,q1) =LSeg(q2,q1) by A11,A5,A15,Th1;
end;
end;
Segment(P,p1,p2,q2,q1) = {p3 where p3 is Point of TOP-REAL 2: LE q2
,p3,P,p1,p2 & LE p3,q1,P,p1,p2} by JORDAN6:26;
then
A16: ex p3 being Point of TOP-REAL 2 st p=p3 & LE q2,p3,P,p1, p2 & LE p3,
q1,P,p1,p2 by A4,A14;
then
A17: LE p,p4,P,p1,p2 by A9,JORDAN5C:13;
A18: for p6 being Point of TOP-REAL 2 st LE p6,p4,P,p1,p2 & LE p,p6,P,p1
,p2 holds p6`1>=e
proof
let p6 be Point of TOP-REAL 2;
assume that
A19: LE p6,p4,P,p1,p2 and
A20: LE p,p6,P,p1,p2;
A21: p6 in P by A19,JORDAN5C:def 3;
now
per cases by A11,A5,A21,Th19;
case
LE q1,p6,P,p1,p2;
hence thesis by A10,A19;
end;
case
A22: LE p6,q1,P,p1,p2;
LE q2,p6,P,p1,p2 by A16,A20,JORDAN5C:13;
then p6 in {qq where qq is Point of TOP-REAL 2: LE q2,qq,P,p1, p2
& LE qq,q1,P,p1,p2} by A22;
then p6 in LSeg(q2,q1) by A14,JORDAN6:26;
hence thesis by A2,A7,GOBOARD7:5;
end;
end;
hence thesis;
end;
p`1=e by A2,A4,A7,GOBOARD7:5;
hence thesis by A3,A4,A11,A8,A17,A18;
end;
case
A23: LE q1,q2,P,p1,p2;
A24: now
per cases;
case
q1<>q2;
then LSeg(q1,q2) is_an_arc_of q1,q2 by TOPREAL1:9;
hence Segment(P,p1,p2,q1,q2) =LSeg(q1,q2) by A3,A11,A23,Th25;
end;
case
A25: q1=q2;
then LSeg(q2,q1)={q1} by RLTOPSP1:70;
hence Segment(P,p1,p2,q1,q2) =LSeg(q1,q2) by A11,A5,A25,Th1;
end;
end;
A26: now
assume LE p4,q2,P,p1,p2;
then p4 in {qq where qq is Point of TOP-REAL 2: LE q1,qq,P,p1,p2 & LE
qq,q2,P,p1,p2} by A9;
then p4 in Segment(P,p1,p2,q1,q2) by JORDAN6:26;
hence contradiction by A2,A7,A8,A24,GOBOARD7:5;
end;
Segment(P,p1,p2,q1,q2) = {p3 where p3 is Point of TOP-REAL 2: LE q1
,p3,P,p1,p2 & LE p3,q2,P,p1,p2} by JORDAN6:26;
then
A27: ex p3 being Point of TOP-REAL 2 st p=p3 & LE q1,p3,P,p1, p2 & LE p3,
q2,P,p1,p2 by A4,A24;
A28: for p6 being Point of TOP-REAL 2 st LE p6,p4,P,p1,p2 & LE p,p6,P,p1
,p2 holds p6`1>=e
proof
let p6 be Point of TOP-REAL 2;
assume that
A29: LE p6,p4,P,p1,p2 and
A30: LE p,p6,P,p1,p2;
LE q1,p6,P,p1,p2 by A27,A30,JORDAN5C:13;
hence thesis by A10,A29;
end;
LE q2,p4,P,p1,p2 or LE p4,q2,P,p1,p2 by A3,A11,A6,A12,Th19;
then
A31: LE p,p4,P,p1,p2 by A27,A26,JORDAN5C:13;
p`1=e by A2,A4,A7,GOBOARD7:5;
hence thesis by A3,A4,A11,A8,A31,A28;
end;
end;
hence thesis;
end;
theorem
for P being non empty Subset of TOP-REAL 2, p1,p2,p being Point of
TOP-REAL 2,e being Real st P is_S-P_arc_joining p1,p2 & p1`1<e & p in P & p`1=e
holds p is_Lin P,p1,p2,e or p is_Rin P,p1,p2,e
proof
let P be non empty Subset of TOP-REAL 2, p1,p2,p be Point of TOP-REAL 2,e be
Real;
assume that
A1: P is_S-P_arc_joining p1,p2 and
A2: p1`1<e and
A3: p in P and
A4: p`1=e;
consider f being FinSequence of (TOP-REAL 2) such that
A5: f is being_S-Seq and
A6: P = L~f and
A7: p1=f/.1 and
A8: p2=f/.len f by A1,TOPREAL4:def 1;
A9: P is_an_arc_of p1,p2 by A1,TOPREAL4:2;
len f >= 2 by A5,TOPREAL1:def 8;
then
A10: len f >1 by XXREAL_0:2;
A11: L~f = union { LSeg(f,i) where i is Nat : 1 <= i & i+1 <= len
f } by TOPREAL1:def 4;
then consider Y being set such that
A12: p in Y and
A13: Y in { LSeg(f,i) where i is Nat : 1 <= i & i+1 <= len f
} by A3,A6,TARSKI:def 4;
consider i being Nat such that
A14: Y=LSeg(f,i) and
A15: 1 <= i and
A16: i+1 <= len f by A13;
A17: i-1>=0 by A15,XREAL_1:48;
A18: 1<i+1 by A15,NAT_1:13;
A19: Y c= L~f
by A11,A13,TARSKI:def 4;
defpred P[Nat] means for p being Point of TOP-REAL 2 st p=f.(i-'$1) holds p
`1<>e;
A20: i<len f by A16,NAT_1:13;
then
A21: i in dom f by A15,FINSEQ_3:25;
A22: 1<len f by A15,A20,XXREAL_0:2;
then 1 in dom f by FINSEQ_3:25;
then f/.1=f.1 by PARTFUN1:def 6;
then
A23: P[i-'1] by A2,A7,A15,NAT_D:58;
then
A24: ex k being Nat st P[k];
ex k being Nat st P[k] & for n being Nat st P[n] holds k <= n from
NAT_1:sch 5(A24);
then consider k being Nat such that
A25: P[k] and
A26: for n being Nat st P[n] holds k <= n;
k<=i-'1 by A23,A26;
then k<=i-1 by A17,XREAL_0:def 2;
then k+1<=i-1+1 by XREAL_1:7;
then
A27: 1+k-k<=i-k by XREAL_1:9;
then
A28: i-'k>=1 by XREAL_0:def 2;
i-'k <=i by NAT_D:35;
then
A29: i-'k <len f by A20,XXREAL_0:2;
then
A30: i-'k in dom f by A28,FINSEQ_3:25;
then
A31: f/.(i-'k)=f.(i-'k) by PARTFUN1:def 6;
then reconsider pk=f.(i-'k) as Point of TOP-REAL 2;
A32: i-'k=i-k by A27,XREAL_0:def 2;
now
per cases by A25,XXREAL_0:1;
case
A33: pk`1<e;
now
per cases;
case
A34: k=0;
set p44=f/.i;
A35: pk=f.i by A34,NAT_D:40
.=p44 by A21,PARTFUN1:def 6;
reconsider ia=i+1 as Nat;
reconsider g=mid(f,i,len f) as FinSequence of (TOP-REAL 2);
A36: i<=len f by A16,NAT_1:13;
ia in Seg len f by A16,A18,FINSEQ_1:1;
then
A37: i+1 in dom f by FINSEQ_1:def 3;
1+(1+i)<=1+len f by A16,XREAL_1:7;
then
A38: 1+1+i-i<=len f+1-i by XREAL_1:9;
then
A39: 1<=len f+1-i by XXREAL_0:2;
A40: len f-i>0 by A20,XREAL_1:50;
then len f-'i=len f-i by XREAL_0:def 2;
then
A41: len f-'i+1>0+1 by A40,XREAL_1:8;
A42: len g=len f -'i+1 by A10,A15,A20,FINSEQ_6:118;
then
A43: 1+1<=len g by A41,NAT_1:13;
then 1+1 in Seg len g by FINSEQ_1:1;
then 1+1 in dom g by FINSEQ_1:def 3;
then
A44: g/.(1+1)=g.(1+1) by PARTFUN1:def 6
.=f.(1+1-1+i) by A15,A20,A38,FINSEQ_6:122
.=f/.(i+1) by A37,PARTFUN1:def 6;
1 in dom g by A42,A41,FINSEQ_3:25;
then
A45: g/.1=g.1 by PARTFUN1:def 6
.=f.(1-1+i) by A15,A36,A39,FINSEQ_6:122
.=f/.i by A21,PARTFUN1:def 6;
LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A15,A16,TOPREAL1:def 3
.=LSeg(g,1) by A43,A45,A44,TOPREAL1:def 3;
then Y in { LSeg(g,i2) where i2 is Nat : 1 <= i2 & i2+1
<= len g } by A14,A43;
then p in union{ LSeg(g,i2) where i2 is Nat : 1 <= i2 &
i2+1 <= len g } by A12,TARSKI:def 4;
then
A46: p in L~mid(f,i,len f) by TOPREAL1:def 4;
A47: LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A15,A16,TOPREAL1:def 3;
A48: for p5 being Point of TOP-REAL 2 st LE p44,p5,P,p1,p2 & LE p5,p
,P,p1,p2 holds p5`1<=e
proof
p44 in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68;
then LSeg(p44,p) c= LSeg(f,i) by A12,A14,A47,TOPREAL1:6;
then
A49: LSeg(p44,p) c= P by A6,A19,A14;
let p5 be Point of TOP-REAL 2;
A50: Segment(P,p1,p2,p44,p)={p8 where p8 is Point of TOP-REAL 2:
LE p44,p8,P,p1,p2 & LE p8,p,P,p1,p2} by JORDAN6:26;
assume LE p44,p5,P,p1,p2 & LE p5,p,P,p1,p2;
then
A51: p5 in Segment(P,p1,p2,p44,p) by A50;
now
per cases;
case
p44<>p;
then LSeg(p44,p) is_an_arc_of p44,p by TOPREAL1:9;
then Segment(P,p1,p2,p44,p)=LSeg(p44,p) by A9,A5,A6,A7,A8,A15
,A20,A46,A49,Th25,SPRECT_4:3;
hence thesis by A4,A33,A35,A51,TOPREAL1:3;
end;
case
p44=p;
hence thesis by A4,A33,A35;
end;
end;
hence thesis;
end;
LE p44,p,P,p1,p2 by A5,A6,A7,A8,A15,A20,A46,SPRECT_4:3;
hence thesis by A3,A4,A9,A33,A35,A48;
end;
case
A52: k<>0;
reconsider ia=i+1 as Nat;
reconsider g=mid(f,i,len f) as FinSequence of (TOP-REAL 2);
A53: i<=len f by A16,NAT_1:13;
ia in Seg len f by A16,A18,FINSEQ_1:1;
then
A54: i+1 in dom f by FINSEQ_1:def 3;
1+(1+i)<=1+len f by A16,XREAL_1:7;
then
A55: 1+1+i-i<=len f+1-i by XREAL_1:9;
then
A56: 1<=len f+1-i by XXREAL_0:2;
A57: len f-i>0 by A20,XREAL_1:50;
then len f-'i=len f-i by XREAL_0:def 2;
then
A58: len f-'i+1>0+1 by A57,XREAL_1:8;
A59: len g=len f -'i+1 by A10,A15,A20,FINSEQ_6:118;
then
A60: 1+1<=len g by A58,NAT_1:13;
then 1+1 in Seg len g by FINSEQ_1:1;
then 1+1 in dom g by FINSEQ_1:def 3;
then
A61: g/.(1+1)=g.(1+1) by PARTFUN1:def 6
.=f.(1+1-1+i) by A15,A20,A55,FINSEQ_6:122
.=f/.(i+1) by A54,PARTFUN1:def 6;
1 in dom g by A59,A58,FINSEQ_3:25;
then
A62: g/.1=g.1 by PARTFUN1:def 6
.=f.(1-1+i) by A15,A53,A56,FINSEQ_6:122
.=f/.i by A21,PARTFUN1:def 6;
LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A15,A16,TOPREAL1:def 3
.=LSeg(g,1) by A60,A62,A61,TOPREAL1:def 3;
then Y in { LSeg(g,i2) where i2 is Nat : 1 <= i2 & i2+1
<= len g } by A14,A60;
then p in union{ LSeg(g,i2) where i2 is Nat : 1 <= i2 &
i2+1 <= len g} by A12,TARSKI:def 4;
then
A63: p in L~mid(f,i,len f) by TOPREAL1:def 4;
reconsider g=mid(f,1,i) as FinSequence of (TOP-REAL 2);
set p44=f/.i;
A64: i<=len f & 1<=i-'k by A16,A27,NAT_1:13,XREAL_0:def 2;
A65: k>=0+1 by A52,NAT_1:13;
then
A66: i-'k<=i+1-1 by A28,NAT_D:51;
A67: i>i-'k by A28,A65,NAT_D:51;
then
A68: i>1 by A28,XXREAL_0:2;
then i-1>0 by XREAL_1:50;
then
A69: i-'1=i-1 by XREAL_0:def 2;
A70: now
assume
A71: (f/.i)`1<>e;
f.i=f/.i by A21,PARTFUN1:def 6;
then
for p9 being Point of TOP-REAL 2 st p9=f.(i-'0) holds p9`1<>e
by A71,NAT_D:40;
hence contradiction by A26,A52;
end;
A72: now
assume not for p51 being Point of TOP-REAL 2 st LE pk,p51,P,p1,
p2 & LE p51,p44,P,p1,p2 holds p51`1<=e;
then consider p51 being Point of TOP-REAL 2 such that
A73: LE pk,p51,P,p1,p2 and
A74: LE p51,p44,P,p1,p2 and
A75: p51`1>e;
p51 in P by A73,JORDAN5C:def 3;
then consider Y3 being set such that
A76: p51 in Y3 and
A77: Y3 in { LSeg(f,i5) where i5 is Nat : 1 <= i5
& i5+1 <= len f } by A6,A11,TARSKI:def 4;
consider kk being Nat such that
A78: Y3=LSeg(f,kk) and
A79: 1 <= kk and
A80: kk+1 <= len f by A77;
A81: LSeg(f,kk)=LSeg(f/.kk,f/.(kk+1)) by A79,A80,TOPREAL1:def 3;
1<kk+1 by A79,NAT_1:13;
then kk+1 in Seg len f by A80,FINSEQ_1:1;
then
A82: kk+1 in dom f by FINSEQ_1:def 3;
A83: kk<len f by A80,NAT_1:13;
then kk in Seg len f by A79,FINSEQ_1:1;
then
A84: kk in dom f by FINSEQ_1:def 3;
A85: LE p51,f/.(kk+1),L~f,f/.1,f/.(len f) by A5,A76,A78,A79,A80,
JORDAN5C:26;
now
per cases by A75,A76,A78,A81,Th2;
case
A86: (f/.kk)`1>e;
A87: LSeg(f/.kk,f/.(kk+1)) c= L~f
proof
let z be object;
assume
A88: z in LSeg(f/.kk,f/.(kk+1));
LSeg(f/.kk,f/.(kk+1)) in { LSeg(f,i7) where i7 is
Nat : 1 <= i7 & i7+1 <= len f } by A79,A80,A81;
hence thesis by A11,A88,TARSKI:def 4;
end;
f is special by A5,TOPREAL1:def 8;
then
A89: (f/.kk)`1=(f/.(kk+1))`1 or (f/.kk)`2=(f/.(kk+1))`2 by A79,A80,
TOPREAL1:def 5;
f is one-to-one & kk<kk+1 by A5,NAT_1:13,TOPREAL1:def 8;
then
A90: f.kk <> f.(kk+1) by A84,A82,FUNCT_1:def 4;
A91: LE f/.(i-'k),p51,L~f,f/.1,f/.(len f) by A6,A7,A8,A30,A73,
PARTFUN1:def 6;
A92: LE f/.(i-'k),f/.(kk+1),L~f,f/.1,f/.(len f) by A6,A7,A8,A31,A73
,A85,JORDAN5C:13;
set k2=i-'kk;
LE f/.kk,p51,L~f,f/.1,f/.(len f) by A5,A76,A78,A79,A80,
JORDAN5C:25;
then
A93: LE f/.kk,p44,L~f,f/.1,f/.(len f) by A6,A7,A8,A74,JORDAN5C:13;
now
assume i-kk<=0;
then i-kk+kk<=0+kk by XREAL_1:7;
then LE f/.i,f/.kk,L~f,f/.1,f/.(len f) by A5,A68,A83,
JORDAN5C:24;
hence contradiction by A1,A6,A7,A8,A70,A86,A93,JORDAN5C:12
,TOPREAL4:2;
end;
then
A94: i-'kk=i-kk by XREAL_0:def 2;
then
A95: i-k2=i-'k2 by XREAL_0:def 2;
i-k2>0 by A79,A94;
then i-'k2>0 by XREAL_0:def 2;
then i-'k2>=0+1 by NAT_1:13;
then P[k2] by A20,A86,A94,A95,FINSEQ_4:15,NAT_D:50;
then k2>=k by A26;
then i-k2<=i-k by XREAL_1:10;
then
A96: LE f/.(i-'k2),f/.(i-'k),L~f,f/.1,f/.(len f ) by A5,A29,A32,A79
,A94,A95,JORDAN5C:24;
f/.kk=f.kk & f/.(kk+1)=f.(kk+1) by A84,A82,PARTFUN1:def 6;
then LSeg(f/.kk,f/.(kk+1)) is_an_arc_of f/.kk,f/.(kk+1) by A90,
TOPREAL1:9;
then
A97: Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1 )) =LSeg(f/.
kk,f/.(kk+1)) by A9,A6,A7,A8,A94,A95,A96,A92,A87,Th25,JORDAN5C:13;
Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1)) ={p8 where
p8 is Point of TOP-REAL 2: LE f/.kk,p8,L~f,f/.1,f/.(len f) & LE p8,f/.(kk+1),L~
f,f/.1,f/.(len f)} by JORDAN6:26;
then
A98: f/.(i-'k) in Segment(L~f,f/.1,f/.(len f),f /.kk,f/.(kk+
1)) by A94,A95,A96,A92;
then (f/.(kk+1))`1<e by A31,A33,A86,A97,Th3;
then (f/.kk)`1> (f/.(kk+1))`1 by A86,XXREAL_0:2;
then (f/.(i-'k))`1>=p51`1 by A5,A76,A78,A79,A83,A81,A91,A98,A97
,A89,Th6;
hence contradiction by A31,A33,A75,XXREAL_0:2;
end;
case
A99: (f/.(kk+1))`1 >e & (f/.kk)`1<=e;
set k2=i-'kk-'1;
A100: LSeg(f/.kk,f/.(kk+1)) c= L~f
proof
let z be object;
assume
A101: z in LSeg(f/.kk,f/.(kk+1));
LSeg(f/.kk,f/.(kk+1)) in { LSeg(f,i7) where i7 is
Nat : 1 <= i7 & i7+1 <= len f } by A79,A80,A81;
hence thesis by A11,A101,TARSKI:def 4;
end;
f is one-to-one & kk<kk+1 by A5,NAT_1:13,TOPREAL1:def 8;
then
A102: f.kk <> f.(kk+1) by A84,A82,FUNCT_1:def 4;
A103: (f/.kk)`1<(f/.(kk+1))`1 by A99,XXREAL_0:2;
LE f/.kk,p51,L~f,f/.1,f/.(len f) by A5,A76,A78,A79,A80,
JORDAN5C:25;
then
A104: LE f/.kk,p44,L~f,f/.1,f/.(len f) by A6,A7,A8,A74,JORDAN5C:13;
f/.kk=f.kk & f/.(kk+1)=f.(kk+1) by A84,A82,PARTFUN1:def 6;
then LSeg(f/.kk,f/.(kk+1)) is_an_arc_of f/.kk,f/.(kk+1) by A102
,TOPREAL1:9;
then
A105: Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1)) ={p8 where
p8 is Point of TOP-REAL 2: LE f/.kk,p8,L~f,f/.1,f/.(len f) & LE p8,f/.(kk+1),L~
f,f/.1,f/.(len f)} & Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1 )) =LSeg(f/.kk,
f/.(kk+1)) by A9,A5,A6,A7,A8,A79,A80,A100,Th25,JORDAN5C:23,JORDAN6:26;
A106: now
assume i-kk-1<=0;
then i-(kk+1)+(kk+1)<=0+(kk+1) by XREAL_1:7;
then LE f/.i,f/.(kk+1),L~f,f/.1,f/.(len f) by A5,A68,A80,
JORDAN5C:24;
then
A107: f/.i in LSeg(f/.kk,f/.(kk+1)) by A105,A104;
f is special by A5,TOPREAL1:def 8;
then
A108: (f/.kk)`1=(f/.(kk+1))`1 or (f/.kk)`2=(f/.(kk+1))`2 by A79,A80
,TOPREAL1:def 5;
LSeg(f,kk)=LSeg(f/.kk,f/.(kk+1)) by A79,A80,TOPREAL1:def 3;
hence contradiction by A5,A6,A7,A8,A70,A74,A75,A76,A78,A79
,A83,A103,A107,A108,Th7;
end;
then i-kk-1+1>=0+1 by XREAL_1:7;
then i-'kk=i-kk by XREAL_0:def 2;
then
A109: i-k2=i-(i-kk-1) by A106,XREAL_0:def 2
.=kk+1;
then i-'k2>0 by XREAL_0:def 2;
then
A110: i-'k2>=0+1 by NAT_1:13;
A111: i-k2=i-'k2 by A109,XREAL_0:def 2;
then P[k2] by A20,A99,A109,A110,FINSEQ_4:15,NAT_D:50;
then k2>=k by A26;
then i-k2<=i-k by XREAL_1:10;
then
A112: LE f/.(kk+1),f/.(i-'k),L~f,f/.1,f/.(len f) by A5,A29,A32,A109
,A111,A110,JORDAN5C:24;
LE f/.(i-'k),f/.(kk+1),L~f,f/.1,f/.(len f) by A6,A7,A8,A31,A73
,A85,JORDAN5C:13;
hence contradiction by A1,A6,A7,A8,A31,A33,A99,A112,JORDAN5C:12
,TOPREAL4:2;
end;
end;
hence contradiction;
end;
A113: LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A15,A16,TOPREAL1:def 3;
A114: for p5 being Point of TOP-REAL 2 st LE p44,p5,P,p1,p2 & LE p5,
p,P,p1,p2 holds p5`1<=e
proof
let p5 be Point of TOP-REAL 2;
A115: Segment(P,p1,p2,p44,p)={p8 where p8 is Point of TOP-REAL 2:
LE p44,p8,P,p1,p2 & LE p8,p,P,p1,p2} by JORDAN6:26;
assume LE p44,p5,P,p1,p2 & LE p5,p,P,p1,p2;
then
A116: p5 in Segment(P,p1,p2,p44,p) by A115;
p44 in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68;
then LSeg(p44,p) c= LSeg(f,i) by A12,A14,A113,TOPREAL1:6;
then
A117: LSeg(p44,p) c= P by A6,A19,A14;
now
per cases;
case
p44<>p;
then LSeg(p44,p) is_an_arc_of p44,p by TOPREAL1:9;
then Segment(P,p1,p2,p44,p)=LSeg(p44,p) by A9,A5,A6,A7,A8,A15
,A20,A63,A117,Th25,SPRECT_4:3;
hence thesis by A4,A70,A116,TOPREAL1:3;
end;
case
p44=p;
then Segment(P,p1,p2,p44,p)={p44} by A1,A3,Th1,TOPREAL4:2;
hence thesis by A70,A116,TARSKI:def 1;
end;
end;
hence thesis;
end;
A118: len g=i -'1+1 by A15,A20,A22,FINSEQ_6:118;
then i-'k+1<=len g by A67,A69,NAT_1:13;
then
A119: LSeg(g,i-'k)=LSeg(g/.(i-'k),g/.(i-'k+1)) by A28,TOPREAL1:def 3;
i-'k <i by A28,A65,NAT_D:51;
then i-'k in Seg len g by A28,A118,A69,FINSEQ_1:1;
then i-'k in dom g by FINSEQ_1:def 3;
then g/.(i-'k)=g.(i-'k) by PARTFUN1:def 6
.=f.(i-'k-1+1) by A15,A64,A66,FINSEQ_6:122
.=f/.(i-'k) by A30,PARTFUN1:def 6;
then
A120: pk in LSeg(g,i-'k) by A31,A119,RLTOPSP1:68;
A121: i-'k+1<=i by A67,NAT_1:13;
1<=(i-'k) by A27,XREAL_0:def 2;
then LSeg(g,i-'k) in { LSeg(g,i2) where i2 is Nat : 1 <=
i2 & i2 +1 <= len g } by A118,A69,A121;
then pk in union{ LSeg(g,i2) where i2 is Nat : 1 <= i2 &
i2+1 <= len g } by A120,TARSKI:def 4;
then pk in L~mid(f,1,i) by TOPREAL1:def 4;
then
A122: LE pk,p44,P,p1,p2 by A5,A6,A7,A8,A20,A68,SPRECT_3:17;
then
A123: p44 in P by JORDAN5C:def 3;
A124: for p5 being Point of TOP-REAL 2 st LE pk,p5,P,p1,p2 & LE p5,p
,P,p1,p2 holds p5`1<=e
proof
let p5 be Point of TOP-REAL 2;
assume that
A125: LE pk,p5,P,p1,p2 and
A126: LE p5,p,P,p1,p2;
A127: p5 in P by A125,JORDAN5C:def 3;
now
per cases by A1,A123,A127,Th19,TOPREAL4:2;
case
LE p5,p44,P,p1,p2;
hence thesis by A72,A125;
end;
case
LE p44,p5,P,p1,p2;
hence thesis by A114,A126;
end;
end;
hence thesis;
end;
LE p44,p,P,p1,p2 by A5,A6,A7,A8,A15,A20,A63,SPRECT_4:3;
then LE pk,p,P,p1,p2 by A122,JORDAN5C:13;
hence thesis by A3,A4,A9,A33,A124;
end;
end;
hence thesis;
end;
case
A128: pk`1>e;
now
per cases;
case
A129: k=0;
set p44=f/.i;
A130: pk=f.i by A129,NAT_D:40
.=p44 by A21,PARTFUN1:def 6;
reconsider ia=i+1 as Nat;
reconsider g=mid(f,i,len f) as FinSequence of (TOP-REAL 2);
A131: i<=len f by A16,NAT_1:13;
ia in Seg len f by A16,A18,FINSEQ_1:1;
then
A132: i+1 in dom f by FINSEQ_1:def 3;
1+(1+i)<=1+len f by A16,XREAL_1:7;
then
A133: 1+1+i-i<=len f+1-i by XREAL_1:9;
then
A134: 1<=len f+1-i by XXREAL_0:2;
A135: len f-i>0 by A20,XREAL_1:50;
then len f-'i=len f-i by XREAL_0:def 2;
then
A136: len f-'i+1>0+1 by A135,XREAL_1:8;
A137: len g=len f -'i+1 by A10,A15,A20,FINSEQ_6:118;
then
A138: 1+1<=len g by A136,NAT_1:13;
then 1+1 in Seg len g by FINSEQ_1:1;
then 1+1 in dom g by FINSEQ_1:def 3;
then
A139: g/.(1+1)=g.(1+1) by PARTFUN1:def 6
.=f.(1+1-1+i) by A15,A20,A133,FINSEQ_6:122
.=f/.(i+1) by A132,PARTFUN1:def 6;
1 in Seg len g by A137,A136,FINSEQ_1:1;
then 1 in dom g by FINSEQ_1:def 3;
then
A140: g/.1=g.1 by PARTFUN1:def 6
.=f.(1-1+i) by A15,A131,A134,FINSEQ_6:122
.=f/.i by A21,PARTFUN1:def 6;
LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A15,A16,TOPREAL1:def 3
.=LSeg(g,1) by A138,A140,A139,TOPREAL1:def 3;
then Y in { LSeg(g,i2) where i2 is Nat : 1 <= i2 & i2+1
<= len g } by A14,A138;
then p in union{ LSeg(g,i2) where i2 is Nat : 1 <= i2 &
i2+1 <= len g } by A12,TARSKI:def 4;
then
A141: p in L~mid(f,i,len f) by TOPREAL1:def 4;
A142: LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A15,A16,TOPREAL1:def 3;
A143: for p5 being Point of TOP-REAL 2 st LE p44,p5,P,p1,p2 & LE p5,
p,P,p1,p2 holds p5`1>=e
proof
p44 in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68;
then LSeg(p44,p) c= LSeg(f,i) by A12,A14,A142,TOPREAL1:6;
then
A144: LSeg(p44,p) c= P by A6,A19,A14;
let p5 be Point of TOP-REAL 2;
A145: Segment(P,p1,p2,p44,p)={p8 where p8 is Point of TOP-REAL 2:
LE p44,p8,P,p1,p2 & LE p8,p,P,p1,p2} by JORDAN6:26;
assume LE p44,p5,P,p1,p2 & LE p5,p,P,p1,p2;
then
A146: p5 in Segment(P,p1,p2,p44,p) by A145;
now
per cases;
case
p44<>p;
then LSeg(p44,p) is_an_arc_of p44,p by TOPREAL1:9;
then Segment(P,p1,p2,p44,p)=LSeg(p44,p) by A9,A5,A6,A7,A8,A15
,A20,A141,A144,Th25,SPRECT_4:3;
hence thesis by A4,A128,A130,A146,TOPREAL1:3;
end;
case
p44=p;
hence thesis by A4,A128,A130;
end;
end;
hence thesis;
end;
LE p44,p,P,p1,p2 by A5,A6,A7,A8,A15,A20,A141,SPRECT_4:3;
hence thesis by A3,A4,A9,A128,A130,A143;
end;
case
A147: k<>0;
reconsider ia=i+1 as Nat;
reconsider g=mid(f,i,len f) as FinSequence of (TOP-REAL 2);
A148: i<=len f by A16,NAT_1:13;
ia in Seg len f by A16,A18,FINSEQ_1:1;
then
A149: i+1 in dom f by FINSEQ_1:def 3;
1+(1+i)<=1+len f by A16,XREAL_1:7;
then
A150: 1+1+i-i<=len f+1-i by XREAL_1:9;
then
A151: 1<=len f+1-i by XXREAL_0:2;
A152: len f-i>0 by A20,XREAL_1:50;
then len f-'i=len f-i by XREAL_0:def 2;
then
A153: len f-'i+1>0+1 by A152,XREAL_1:8;
A154: len g=len f -'i+1 by A10,A15,A20,FINSEQ_6:118;
then
A155: 1+1<=len g by A153,NAT_1:13;
then 1+1 in Seg len g by FINSEQ_1:1;
then 1+1 in dom g by FINSEQ_1:def 3;
then
A156: g/.(1+1)=g.(1+1) by PARTFUN1:def 6
.=f.(1+1-1+i) by A15,A20,A150,FINSEQ_6:122
.=f/.(i+1) by A149,PARTFUN1:def 6;
1 in Seg len g by A154,A153,FINSEQ_1:1;
then 1 in dom g by FINSEQ_1:def 3;
then
A157: g/.1=g.1 by PARTFUN1:def 6
.=f.(1-1+i) by A15,A148,A151,FINSEQ_6:122
.=f/.i by A21,PARTFUN1:def 6;
LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A15,A16,TOPREAL1:def 3
.=LSeg(g,1) by A155,A157,A156,TOPREAL1:def 3;
then Y in { LSeg(g,i2) where i2 is Nat : 1 <= i2 & i2+1
<= len g } by A14,A155;
then p in union{ LSeg(g,i2) where i2 is Nat : 1 <= i2 &
i2+1 <= len g } by A12,TARSKI:def 4;
then
A158: p in L~mid(f,i,len f) by TOPREAL1:def 4;
reconsider g=mid(f,1,i) as FinSequence of (TOP-REAL 2);
set p44=f/.i;
A159: i<=len f & 1<=i-'k by A16,A27,NAT_1:13,XREAL_0:def 2;
A160: k>=0+1 by A147,NAT_1:13;
then
A161: i-'k<=i+1-1 by A28,NAT_D:51;
A162: i>i-'k by A28,A160,NAT_D:51;
then
A163: i>1 by A28,XXREAL_0:2;
then i-1>0 by XREAL_1:50;
then
A164: i-'1=i-1 by XREAL_0:def 2;
A165: now
assume
A166: (f/.i)`1<>e;
f.i=f/.i by A21,PARTFUN1:def 6;
then for p9 being Point of TOP-REAL 2 st p9=f.(i-'0) holds p9`1<>
e by A166,NAT_D:40;
hence contradiction by A26,A147;
end;
A167: now
assume not for p51 being Point of TOP-REAL 2 st LE pk,p51,P,p1,
p2 & LE p51,p44,P,p1,p2 holds p51`1>=e;
then consider p51 being Point of TOP-REAL 2 such that
A168: LE pk,p51,P,p1,p2 and
A169: LE p51,p44,P,p1,p2 and
A170: p51`1<e;
p51 in P by A168,JORDAN5C:def 3;
then consider Y3 being set such that
A171: p51 in Y3 and
A172: Y3 in { LSeg(f,i5) where i5 is Nat : 1 <= i5
& i5+1 <= len f } by A6,A11,TARSKI:def 4;
consider kk being Nat such that
A173: Y3=LSeg(f,kk) and
A174: 1 <= kk and
A175: kk+1 <= len f by A172;
A176: LSeg(f,kk)=LSeg(f/.kk,f/.(kk+1)) by A174,A175,TOPREAL1:def 3;
1<kk+1 by A174,NAT_1:13;
then kk+1 in Seg len f by A175,FINSEQ_1:1;
then
A177: kk+1 in dom f by FINSEQ_1:def 3;
A178: kk<len f by A175,NAT_1:13;
then kk in Seg len f by A174,FINSEQ_1:1;
then
A179: kk in dom f by FINSEQ_1:def 3;
A180: LE p51,f/.(kk+1),L~f,f/.1,f/.(len f) by A5,A171,A173,A174,A175,
JORDAN5C:26;
now
per cases by A170,A171,A173,A176,Th3;
case
A181: (f/.kk)`1<e;
set k2=i-'kk;
LE f/.kk,p51,L~f,f/.1,f/.(len f) by A5,A171,A173,A174,A175,
JORDAN5C:25;
then
A182: LE f/.kk,p44,L~f,f/.1,f/.(len f) by A6,A7,A8,A169,JORDAN5C:13;
now
assume i-kk<=0;
then i-kk+kk<=0+kk by XREAL_1:7;
then
LE f/.i,f/.kk,L~f,f/.1,f/.(len f) by A5,A163,A178,JORDAN5C:24;
hence contradiction by A1,A6,A7,A8,A165,A181,A182,JORDAN5C:12
,TOPREAL4:2;
end;
then
A183: i-k2=i-(i-kk) by XREAL_0:def 2
.=kk;
then
A184: i-k2=i-'k2 by XREAL_0:def 2;
then P[k2] by A20,A174,A181,A183,FINSEQ_4:15,NAT_D:50;
then k2>=k by A26;
then i-k2<=i-k by XREAL_1:10;
then
A185: LE f/.(i-'k2),f/.(i-'k),L~f,f/.1,f/.(len f ) by A5,A29,A32,A174
,A183,A184,JORDAN5C:24;
A186: LSeg(f/.kk,f/.(kk+1)) c= L~f
proof
let z be object;
assume
A187: z in LSeg(f/.kk,f/.(kk+1));
LSeg(f/.kk,f/.(kk+1)) in { LSeg(f,i7) where i7 is
Nat : 1 <= i7 & i7+1 <= len f } by A174,A175,A176;
hence thesis by A11,A187,TARSKI:def 4;
end;
f is special by A5,TOPREAL1:def 8;
then
A188: (f/.kk)`1=(f/.(kk+1))`1 or (f/.kk)`2=(f/.(kk+1))`2 by A174,A175
,TOPREAL1:def 5;
f is one-to-one & kk<kk+1 by A5,NAT_1:13,TOPREAL1:def 8;
then
A189: f.kk <> f.(kk+1) by A179,A177,FUNCT_1:def 4;
A190: LE f/.(i-'k),p51,L~f,f/.1,f/.(len f) by A6,A7,A8,A30,A168,
PARTFUN1:def 6;
A191: LE f/.(i-'k),f/.(kk+1),L~f,f/.1,f/.(len f) by A6,A7,A8,A31,A168
,A180,JORDAN5C:13;
f/.kk=f.kk & f/.(kk+1)=f.(kk+1) by A179,A177,PARTFUN1:def 6;
then LSeg(f/.kk,f/.(kk+1)) is_an_arc_of f/.kk,f/.(kk+1) by A189
,TOPREAL1:9;
then
A192: Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1 )) =LSeg(f/.
kk,f/.(kk+1)) by A9,A6,A7,A8,A183,A184,A185,A191,A186,Th25,JORDAN5C:13;
Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1)) ={p8 where
p8 is Point of TOP-REAL 2: LE f/.kk,p8,L~f,f/.1,f/.(len f) & LE p8,f/.(kk+1),L~
f,f/.1,f/.(len f)} by JORDAN6:26;
then
A193: f/.(i-'k) in Segment(L~f,f/.1,f/.(len f),f /.kk,f/.(kk+
1)) by A183,A184,A185,A191;
then (f/.(kk+1))`1>e by A31,A128,A181,A192,Th2;
then (f/.kk)`1< (f/.(kk+1))`1 by A181,XXREAL_0:2;
then (f/.(i-'k))`1<=p51`1 by A5,A171,A173,A174,A178,A176,A190
,A193,A192,A188,Th7;
hence contradiction by A31,A128,A170,XXREAL_0:2;
end;
case
A194: (f/.(kk+1))`1 <e & (f/.kk)`1>=e;
set k2=i-'kk-'1;
A195: LSeg(f/.kk,f/.(kk+1)) c= L~f
proof
let z be object;
assume
A196: z in LSeg(f/.kk,f/.(kk+1));
LSeg(f/.kk,f/.(kk+1)) in { LSeg(f,i7) where i7 is
Nat : 1 <= i7 & i7+1 <= len f } by A174,A175,A176;
hence thesis by A11,A196,TARSKI:def 4;
end;
f is one-to-one & kk<kk+1 by A5,NAT_1:13,TOPREAL1:def 8;
then
A197: f.kk <> f.(kk+1) by A179,A177,FUNCT_1:def 4;
A198: (f/.kk)`1>(f/.(kk+1))`1 by A194,XXREAL_0:2;
LE f/.kk,p51,L~f,f/.1,f/.(len f) by A5,A171,A173,A174,A175,
JORDAN5C:25;
then
A199: LE f/.kk,p44,L~f,f/.1,f/.(len f) by A6,A7,A8,A169,JORDAN5C:13;
f/.kk=f.kk & f/.(kk+1)=f.(kk+1) by A179,A177,PARTFUN1:def 6;
then LSeg(f/.kk,f/.(kk+1)) is_an_arc_of f/.kk,f/.(kk+1) by A197
,TOPREAL1:9;
then
A200: Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1)) ={p8 where
p8 is Point of TOP-REAL 2: LE f/.kk,p8,L~f,f/.1,f/.(len f) & LE p8,f/.(kk+1),L~
f,f/.1,f/.(len f)} & Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1 )) =LSeg(f/.kk,
f/.(kk+1)) by A9,A5,A6,A7,A8,A174,A175,A195,Th25,JORDAN5C:23,JORDAN6:26;
A201: now
assume i-kk-1<=0;
then i-(kk+1)+(kk+1)<=0+(kk+1) by XREAL_1:7;
then LE f/.i,f/.(kk+1),L~f,f/.1,f/.(len f) by A5,A163,A175,
JORDAN5C:24;
then
A202: f/.i in LSeg(f/.kk,f/.(kk+1)) by A200,A199;
f is special by A5,TOPREAL1:def 8;
then
A203: (f/.kk)`1=(f/.(kk+1))`1 or (f/.kk)`2=(f/.(kk+1))`2 by A174
,A175,TOPREAL1:def 5;
LSeg(f,kk)=LSeg(f/.kk,f/.(kk+1)) by A174,A175,TOPREAL1:def 3;
hence contradiction by A5,A6,A7,A8,A165,A169,A170,A171,A173
,A174,A178,A198,A202,A203,Th6;
end;
then i-kk-1+1>=0+1 by XREAL_1:7;
then i-'kk=i-kk by XREAL_0:def 2;
then
A204: i-k2=i-(i-kk-1) by A201,XREAL_0:def 2
.=kk+1;
then i-'k2>0 by XREAL_0:def 2;
then
A205: i-'k2>=0+1 by NAT_1:13;
A206: i-k2=i-'k2 by A204,XREAL_0:def 2;
then P[k2] by A20,A194,A204,A205,FINSEQ_4:15,NAT_D:50;
then k2>=k by A26;
then i-k2<=i-k by XREAL_1:10;
then
A207: LE f/.(kk+1),f/.(i-'k),L~f,f/.1,f/.(len f) by A5,A29,A32,A204
,A206,A205,JORDAN5C:24;
LE f/.(i-'k),f/.(kk+1),L~f,f/.1,f/.(len f) by A6,A7,A8,A31,A168
,A180,JORDAN5C:13;
hence contradiction by A1,A6,A7,A8,A31,A128,A194,A207,
JORDAN5C:12,TOPREAL4:2;
end;
end;
hence contradiction;
end;
A208: LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A15,A16,TOPREAL1:def 3;
A209: for p5 being Point of TOP-REAL 2 st LE p44,p5,P,p1,p2 & LE p5,
p,P,p1,p2 holds p5`1>=e
proof
let p5 be Point of TOP-REAL 2;
A210: Segment(P,p1,p2,p44,p)={p8 where p8 is Point of TOP-REAL 2:
LE p44,p8,P,p1,p2 & LE p8,p,P,p1,p2} by JORDAN6:26;
assume LE p44,p5,P,p1,p2 & LE p5,p,P,p1,p2;
then
A211: p5 in Segment(P,p1,p2,p44,p) by A210;
p44 in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68;
then LSeg(p44,p) c= LSeg(f,i) by A12,A14,A208,TOPREAL1:6;
then
A212: LSeg(p44,p) c= P by A6,A19,A14;
now
per cases;
case
p44<>p;
then LSeg(p44,p) is_an_arc_of p44,p by TOPREAL1:9;
then Segment(P,p1,p2,p44,p)=LSeg(p44,p) by A9,A5,A6,A7,A8,A15
,A20,A158,A212,Th25,SPRECT_4:3;
hence thesis by A4,A165,A211,TOPREAL1:3;
end;
case
p44=p;
then Segment(P,p1,p2,p44,p)={p44} by A1,A3,Th1,TOPREAL4:2;
hence thesis by A165,A211,TARSKI:def 1;
end;
end;
hence thesis;
end;
A213: len g=i -'1+1 by A15,A20,A22,FINSEQ_6:118;
then i-'k+1<=len g by A162,A164,NAT_1:13;
then
A214: LSeg(g,i-'k)=LSeg(g/.(i-'k),g/.(i-'k+1)) by A28,TOPREAL1:def 3;
i-'k <i by A28,A160,NAT_D:51;
then i-'k in Seg len g by A28,A213,A164,FINSEQ_1:1;
then i-'k in dom g by FINSEQ_1:def 3;
then g/.(i-'k)=g.(i-'k) by PARTFUN1:def 6
.=f.(i-'k-1+1) by A15,A159,A161,FINSEQ_6:122
.=f/.(i-'k) by A30,PARTFUN1:def 6;
then
A215: pk in LSeg(g,i-'k) by A31,A214,RLTOPSP1:68;
A216: i-'k+1<=i by A162,NAT_1:13;
1<=(i-'k) by A27,XREAL_0:def 2;
then LSeg(g,i-'k) in { LSeg(g,i2) where i2 is Nat : 1 <=
i2 & i2 +1 <= len g } by A213,A164,A216;
then pk in union{ LSeg(g,i2) where i2 is Nat : 1 <= i2 &
i2+1 <= len g } by A215,TARSKI:def 4;
then pk in L~mid(f,1,i) by TOPREAL1:def 4;
then
A217: LE pk,p44,P,p1,p2 by A5,A6,A7,A8,A20,A163,SPRECT_3:17;
then
A218: p44 in P by JORDAN5C:def 3;
A219: for p5 being Point of TOP-REAL 2 st LE pk,p5,P,p1,p2 & LE p5,p
,P,p1,p2 holds p5`1>=e
proof
let p5 be Point of TOP-REAL 2;
assume that
A220: LE pk,p5,P,p1,p2 and
A221: LE p5,p,P,p1,p2;
A222: p5 in P by A220,JORDAN5C:def 3;
now
per cases by A1,A218,A222,Th19,TOPREAL4:2;
case
LE p5,p44,P,p1,p2;
hence thesis by A167,A220;
end;
case
LE p44,p5,P,p1,p2;
hence thesis by A209,A221;
end;
end;
hence thesis;
end;
LE p44,p,P,p1,p2 by A5,A6,A7,A8,A15,A20,A158,SPRECT_4:3;
then LE pk,p,P,p1,p2 by A217,JORDAN5C:13;
hence thesis by A3,A4,A9,A128,A219;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem
for P being non empty Subset of TOP-REAL 2, p1,p2,p being Point of
TOP-REAL 2,e being Real st P is_S-P_arc_joining p1,p2 & p2`1>e & p in P & p`1=e
holds p is_Lout P,p1,p2,e or p is_Rout P,p1,p2,e
proof
let P be non empty Subset of TOP-REAL 2, p1,p2,p be Point of TOP-REAL 2,e be
Real;
assume that
A1: P is_S-P_arc_joining p1,p2 and
A2: p2`1>e and
A3: p in P and
A4: p`1=e;
consider f being FinSequence of (TOP-REAL 2) such that
A5: f is being_S-Seq and
A6: P = L~f and
A7: p1=f/.1 and
A8: p2=f/.len f by A1,TOPREAL4:def 1;
A9: P is_an_arc_of p1,p2 by A1,TOPREAL4:2;
A10: L~f = union { LSeg(f,i) where i is Nat : 1 <= i & i+1 <= len
f } by TOPREAL1:def 4;
then consider Y being set such that
A11: p in Y and
A12: Y in { LSeg(f,i) where i is Nat : 1 <= i & i+1 <= len f
} by A3,A6,TARSKI:def 4;
consider i being Nat such that
A13: Y=LSeg(f,i) and
A14: 1 <= i and
A15: i+1 <= len f by A12;
A16: 1<i+1 by A14,NAT_1:13;
A17: 1<i+1 by A14,NAT_1:13;
then i+1 in Seg len f by A15,FINSEQ_1:1;
then
A18: i+1 in dom f by FINSEQ_1:def 3;
A19: Y c= L~f
by A10,A12,TARSKI:def 4;
defpred P[Nat] means for p being Point of TOP-REAL 2 st p=f.(i+1+$1) holds p
`1<>e;
A20: len f - (i+1)>=0 by A15,XREAL_1:48;
then
A21: i+1+((len f)-'(i+1))=i+1+(len f -(i+1)) by XREAL_0:def 2
.=len f;
A22: len f -'(i+1)=len f -(i+1) by A20,XREAL_0:def 2;
A23: i<len f by A15,NAT_1:13;
then 1<len f by A14,XXREAL_0:2;
then len f in Seg len f by FINSEQ_1:1;
then len f in dom f by FINSEQ_1:def 3;
then
A24: P[(len f)-'(i+1)] by A2,A8,A21,PARTFUN1:def 6;
then
A25: ex k being Nat st P[k];
ex k being Nat st P[k] & for n being Nat st P[n] holds k <= n from
NAT_1:sch 5(A25);
then consider k being Nat such that
A26: P[k] and
A27: for n being Nat st P[n] holds k <= n;
k<=len f -'(i+1) by A24,A27;
then
A28: k+(i+1)<= len f -(i+1)+(i+1) by A22,XREAL_1:7;
i+k >=i by NAT_1:11;
then
A29: i+k+1 >=i+1 by XREAL_1:7;
then
A30: i+1+k >1 by A16,XXREAL_0:2;
1<=i+1+k by A17,NAT_1:12;
then i+1+k in Seg len f by A28,FINSEQ_1:1;
then
A31: i+1+k in dom f by FINSEQ_1:def 3;
then
A32: f/.(i+1+k)=f.(i+1+k) by PARTFUN1:def 6;
then reconsider pk=f.(i+1+k) as Point of TOP-REAL 2;
A33: k+i+1>1 by A16,A29,XXREAL_0:2;
now
per cases by A26,XXREAL_0:1;
case
A34: pk`1<e;
now
per cases;
case
A35: k=0;
set p44=f/.(i+1);
A36: pk=p44 by A18,A35,PARTFUN1:def 6;
A37: p44 in LSeg(p,f/.(i+1)) by RLTOPSP1:68;
A38: LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A14,A15,TOPREAL1:def 3;
A39: for p5 being Point of TOP-REAL 2 st LE p5,p44,P,p1,p2 & LE p,p5
,P,p1,p2 holds p5`1<=e
proof
p44 in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68;
then LSeg(p,p44) c= LSeg(f,i) by A11,A13,A38,TOPREAL1:6;
then
A40: LSeg(p,p44) c= P by A6,A19,A13;
let p5 be Point of TOP-REAL 2;
A41: Segment(P,p1,p2,p,p44)={p8 where p8 is Point of TOP-REAL 2:
LE p,p8,P,p1,p2 & LE p8,p44,P,p1,p2} by JORDAN6:26;
assume LE p5,p44,P,p1,p2 & LE p,p5,P,p1,p2;
then
A42: p5 in Segment(P,p1,p2,p,p44) by A41;
now
per cases;
case
p44<>p;
then LSeg(p,p44) is_an_arc_of p,p44 by TOPREAL1:9;
then
Segment(P,p1,p2,p,p44)=LSeg(p,p44) by A9,A5,A6,A7,A8,A11,A13
,A14,A23,A37,A40,Th25,SPRECT_4:4;
hence thesis by A4,A34,A36,A42,TOPREAL1:3;
end;
case
p44=p;
hence thesis by A4,A18,A34,A35,PARTFUN1:def 6;
end;
end;
hence thesis;
end;
LE p,p44,P,p1,p2 by A5,A6,A7,A8,A11,A13,A14,A23,A37,SPRECT_4:4;
hence thesis by A3,A4,A9,A34,A36,A39;
end;
case
A43: k<>0;
set p44=f/.(i+1);
A44: now
assume (f/.(i+1))`1<>e;
then
for p9 being Point of TOP-REAL 2 st p9=f.(i+1+0) holds p9`1<>
e by A18,PARTFUN1:def 6;
hence contradiction by A27,A43;
end;
A45: LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A14,A15,TOPREAL1:def 3;
A46: now
assume not for p51 being Point of TOP-REAL 2 st LE p44,p51,P,p1,
p2 & LE p51,pk,P,p1,p2 holds p51`1<=e;
then consider p51 being Point of TOP-REAL 2 such that
A47: LE p44,p51,P,p1,p2 and
A48: LE p51,pk,P,p1,p2 and
A49: p51`1>e;
p51 in P by A47,JORDAN5C:def 3;
then consider Y3 being set such that
A50: p51 in Y3 and
A51: Y3 in { LSeg(f,i5) where i5 is Nat : 1 <= i5 &
i5+1 <= len f } by A6,A10,TARSKI:def 4;
consider kk being Nat such that
A52: Y3=LSeg(f,kk) and
A53: 1 <= kk and
A54: kk+1 <= len f by A51;
A55: LE p51,f/.(kk+1),L~f,f/.1,f/.(len f) by A5,A50,A52,A53,A54,
JORDAN5C:26;
A56: LE f/.kk,p51,L~f,f/.1,f/.(len f) by A5,A50,A52,A53,A54,JORDAN5C:25;
A57: kk-1>=0 by A53,XREAL_1:48;
A58: LSeg(f,kk)=LSeg(f/.kk,f/.(kk+1)) by A53,A54,TOPREAL1:def 3;
A59: kk<len f by A54,NAT_1:13;
then
A60: kk in dom f by A53,FINSEQ_3:25;
then
A61: f/.kk=f.kk by PARTFUN1:def 6;
A62: 1<kk+1 by A53,NAT_1:13;
then
A63: kk+1 in dom f by A54,FINSEQ_3:25;
f is one-to-one & kk<kk+1 by A5,NAT_1:13,TOPREAL1:def 8;
then
A64: f.kk <> f.(kk+1) by A60,A63,FUNCT_1:def 4;
now
per cases by A49,A50,A52,A58,Th2;
case
A65: (f/.(kk+1))`1>e;
set k2=kk-'i;
A66: LE p44,f/.(kk+1),L~f,f/.1,f/.(len f) by A6,A7,A8,A47,A55,
JORDAN5C:13;
now
assume kk-i<0;
then kk-i+i<0+i by XREAL_1:6;
then LE f/.(kk+1),f/.(i+1),L~f,f/.1,f/.(len f) by A5,A15,A62,
JORDAN5C:24,XREAL_1:7;
hence contradiction by A1,A6,A7,A8,A44,A65,A66,JORDAN5C:12
,TOPREAL4:2;
end;
then
A67: i+1+k2=1+i+(kk-i) by XREAL_0:def 2
.=kk+1;
A68: LSeg(f/.kk,f/.(kk+1)) c= L~f
proof
let z be object;
assume
A69: z in LSeg(f/.kk,f/.(kk+1));
LSeg(f/.kk,f/.(kk+1)) in { LSeg(f,i7) where i7 is
Nat : 1 <= i7 & i7+1 <= len f } by A53,A54,A58;
hence thesis by A10,A69,TARSKI:def 4;
end;
f is special by A5,TOPREAL1:def 8;
then
A70: (f/.kk)`1=(f/.(kk+1))`1 or (f/.kk)`2=(f/.(kk+1))`2 by A53,A54,
TOPREAL1:def 5;
f is one-to-one & kk<kk+1 by A5,NAT_1:13,TOPREAL1:def 8;
then
A71: f.kk <> f.(kk+1) by A60,A63,FUNCT_1:def 4;
A72: LE p51,f/.(i+1+k),L~f,f/.1,f/.(len f) by A6,A7,A8,A31,A48,
PARTFUN1:def 6;
A73: LE f/.(kk),f/.(i+1+k),L~f,f/.1,f/.(len f) by A6,A7,A8,A32,A48
,A56,JORDAN5C:13;
1<kk+1 by A53,NAT_1:13;
then P[k2] by A54,A65,A67,FINSEQ_4:15;
then k2>=k by A27;
then
A74: LE f/.(i+1+k),f/.(i+1+k2),L~f,f/.1,f/.(len f) by A5,A33,A54,A67
,JORDAN5C:24,XREAL_1:7;
f/.kk=f.kk & f/.(kk+1)=f.(kk+1) by A60,A63,PARTFUN1:def 6;
then LSeg(f/.kk,f/.(kk+1)) is_an_arc_of f/.kk,f/.(kk+1) by A71,
TOPREAL1:9;
then
A75: Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1 )) =LSeg(f/.
kk,f/.(kk+1)) by A9,A6,A7,A8,A67,A74,A73,A68,Th25,JORDAN5C:13;
Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1)) ={p8 where
p8 is Point of TOP-REAL 2: LE f/.kk,p8,L~f,f/.1,f/.(len f) & LE p8,f/.(kk+1),L~
f,f/.1,f/.(len f)} by JORDAN6:26;
then
A76: f/.(i+1+k) in Segment(L~f,f/.1,f/.(len f), f/.kk,f/.(kk
+ 1)) by A67,A74,A73;
then (f/.(kk))`1<e by A32,A34,A65,A75,Th3;
then (f/.kk)`1< (f/.(kk+1))`1 by A65,XXREAL_0:2;
then (f/.(i+1+k))`1>=p51`1 by A5,A50,A52,A53,A59,A58,A72,A76
,A75,A70,Th7;
hence contradiction by A32,A34,A49,XXREAL_0:2;
end;
case
A77: (f/.(kk))`1 >e & (f/.(kk+1))`1<=e;
set k2=kk-'(i+1);
A78: LSeg(f/.kk,f/.(kk+1)) c= L~f
proof
let z be object;
assume
A79: z in LSeg(f/.kk,f/.(kk+1));
LSeg(f/.kk,f/.(kk+1)) in { LSeg(f,i7) where i7 is
Nat : 1 <= i7 & i7+1 <= len f } by A53,A54,A58;
hence thesis by A10,A79,TARSKI:def 4;
end;
LE p51,f/.(kk+1),L~f,f/.1,f/.(len f) by A5,A50,A52,A53,A54,
JORDAN5C:26;
then
A80: LE p44,f/.(kk+1),L~f,f/.1,f/.(len f) by A6,A7,A8,A47,
JORDAN5C:13;
f/.(kk+1)=f.(kk+1) by A63,PARTFUN1:def 6;
then LSeg(f/.kk,f/.(kk+1)) is_an_arc_of f/.kk,f/.(kk+1) by A64
,A61,TOPREAL1:9;
then
A81: Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1)) ={p8 where
p8 is Point of TOP-REAL 2: LE f/.kk,p8,L~f,f/.1,f/.(len f) & LE p8,f/.(kk+1),L~
f,f/.1,f/.(len f)} & Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1 )) =LSeg(f/.kk,
f/.(kk+1)) by A9,A5,A6,A7,A8,A53,A54,A78,Th25,JORDAN5C:23,JORDAN6:26;
A82: now
assume kk-(i+1)<0;
then kk-(i+1)+(i+1)<0+(i+1) by XREAL_1:6;
then kk<=i by NAT_1:13;
then
A83: LE f/.kk,f/.i,L~f,f/.1,f/.(len f) by A5,A23,A53,JORDAN5C:24;
A84: f/.i in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68;
LE f/.i,p44,L~f,f/.1,f/.(len f) by A5,A14,A15,JORDAN5C:23;
then LE f/.i,f/.(kk+1),L~f,f/.1,f/.(len f) by A80,JORDAN5C:13
;
then f/.i in LSeg(f/.kk,f/.(kk+1)) by A81,A83;
then LSeg(f/.kk,f/.(kk+1)) /\ LSeg(f/.i,f/.(i+1))<>{} by A84,
XBOOLE_0:def 4;
then
A85: not LSeg(f/.kk,f/.(kk+1)) misses LSeg (f/.i,f/.(i+1) )
by XBOOLE_0:def 7;
A86: kk-1=kk-'1 by A57,XREAL_0:def 2;
A87: now
assume
A88: i=kk-'1+2;
then kk+1<i+1 by A86,NAT_1:13;
then LE f/.(kk+1),p44,L~f,f/.1,f/.(len f) by A5,A15,A62,
JORDAN5C:24;
then p44=f/.(kk+1) by A1,A6,A7,A8,A80,JORDAN5C:12
,TOPREAL4:2;
then f.(i+1)=f/.(kk+1) by A18,PARTFUN1:def 6;
then
A89: f.(i+1)=f.(kk+1) by A63,PARTFUN1:def 6;
f is one-to-one by A5,TOPREAL1:def 8;
then i+1=kk+1 by A18,A63,A89,FUNCT_1:def 4;
hence contradiction by A86,A88;
end;
A90: f is s.n.c. by A5,TOPREAL1:def 8;
A91: LSeg(f,kk)=LSeg(f/.kk,f/.(kk+1)) & LSeg(f,i)=LSeg(f/.i
,f/.(i+1)) by A14,A15,A53,A54,TOPREAL1:def 3;
then i+1>=kk by A85,A90,TOPREAL1:def 7;
then
A92: i+1-1>=kk-1 by XREAL_1:9;
kk+1>=i by A85,A91,A90,TOPREAL1:def 7;
then
A93: i=kk-'1+0 or ... or i=kk-'1+2 by A86,A92,NAT_1:62;
A94: now
per cases by A86,A93,A87;
case
i=kk;
hence p44 in LSeg(f,kk) by A45,RLTOPSP1:68;
end;
case
i=kk-1;
hence p44 in LSeg(f,kk) by A58,RLTOPSP1:68;
end;
end;
f is special by A5,TOPREAL1:def 8;
then (f/.kk)`1=(f/.(kk+1))`1 or (f/.kk)`2=(f/.(kk+1))`2 by
A53,A54,TOPREAL1:def 5;
hence contradiction by A5,A6,A7,A8,A44,A47,A49,A50,A52,A53
,A59,A77,A94,Th6;
end;
then i+1+k2=i+1+(kk-(i+1)) by XREAL_0:def 2
.=kk;
then P[k2] by A53,A59,A77,FINSEQ_4:15;
then
A95: k2>=k by A27;
kk-'(i+1)=kk-(i+1) by A82,XREAL_0:def 2;
then kk-(i+1)+(i+1)>=k+(i+1) by A95,XREAL_1:7;
then
A96: LE f/.(i+1+k),f/.(kk),L~f,f/.1,f/.(len f) by A5,A30,A59,
JORDAN5C:24;
LE f/.(kk),f/.(i+1+k),L~f,f/.1,f/.(len f) by A6,A7,A8,A32,A48
,A56,JORDAN5C:13;
hence contradiction by A1,A6,A7,A8,A32,A34,A77,A96,JORDAN5C:12
,TOPREAL4:2;
end;
end;
hence contradiction;
end;
A97: p44 in LSeg(p,f/.(i+1)) by RLTOPSP1:68;
A98: for p5 being Point of TOP-REAL 2 st LE p,p5,P,p1,p2 & LE p5,p44
,P,p1,p2 holds p5`1<=e
proof
let p5 be Point of TOP-REAL 2;
A99: Segment(P,p1,p2,p,p44)={p8 where p8 is Point of TOP-REAL 2:
LE p,p8,P,p1,p2 & LE p8,p44,P,p1,p2} by JORDAN6:26;
assume LE p,p5,P,p1,p2 & LE p5,p44,P,p1,p2;
then
A100: p5 in Segment(P,p1,p2,p,p44) by A99;
p44 in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68;
then LSeg(p,p44) c= LSeg(f,i) by A11,A13,A45,TOPREAL1:6;
then
A101: LSeg(p,p44) c= P by A6,A19,A13;
now
per cases;
case
p44<>p;
then LSeg(p,p44) is_an_arc_of p,p44 by TOPREAL1:9;
then
Segment(P,p1,p2,p,p44)=LSeg(p,p44) by A9,A5,A6,A7,A8,A11,A13
,A14,A23,A97,A101,Th25,SPRECT_4:4;
hence thesis by A4,A44,A100,TOPREAL1:3;
end;
case
p44=p;
then Segment(P,p1,p2,p,p44)={p44} by A1,A3,Th1,TOPREAL4:2;
hence thesis by A44,A100,TARSKI:def 1;
end;
end;
hence thesis;
end;
i+1<=i+1+k by NAT_1:11;
then
A102: LE p44,pk,P,p1,p2 by A5,A6,A7,A8,A17,A28,A32,JORDAN5C:24;
then
A103: p44 in P by JORDAN5C:def 3;
A104: for p5 being Point of TOP-REAL 2 st LE p5,pk,P,p1,p2 & LE p,p5
,P,p1,p2 holds p5`1<=e
proof
let p5 be Point of TOP-REAL 2;
assume that
A105: LE p5,pk,P,p1,p2 and
A106: LE p,p5,P,p1,p2;
A107: p5 in P by A105,JORDAN5C:def 3;
now
per cases by A1,A103,A107,Th19,TOPREAL4:2;
case
LE p44,p5,P,p1,p2;
hence thesis by A46,A105;
end;
case
LE p5,p44,P,p1,p2;
hence thesis by A98,A106;
end;
end;
hence thesis;
end;
LE p,p44,P,p1,p2 by A5,A6,A7,A8,A11,A13,A14,A23,A97,SPRECT_4:4;
then LE p,pk,P,p1,p2 by A102,JORDAN5C:13;
hence thesis by A3,A4,A9,A34,A104;
end;
end;
hence thesis;
end;
case
A108: pk`1>e;
now
per cases;
case
A109: k=0;
set p44=f/.(i+1);
A110: pk=p44 by A18,A109,PARTFUN1:def 6;
A111: p44 in LSeg(p,f/.(i+1)) by RLTOPSP1:68;
A112: LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A14,A15,TOPREAL1:def 3;
A113: for p5 being Point of TOP-REAL 2 st LE p5,p44,P,p1,p2 & LE p,
p5,P,p1,p2 holds p5`1>=e
proof
p44 in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68;
then LSeg(p,p44) c= LSeg(f,i) by A11,A13,A112,TOPREAL1:6;
then
A114: LSeg(p,p44) c= P by A6,A19,A13;
let p5 be Point of TOP-REAL 2;
A115: Segment(P,p1,p2,p,p44)={p8 where p8 is Point of TOP-REAL 2:
LE p,p8,P,p1,p2 & LE p8,p44,P,p1,p2} by JORDAN6:26;
assume LE p5,p44,P,p1,p2 & LE p,p5,P,p1,p2;
then
A116: p5 in Segment(P,p1,p2,p,p44) by A115;
now
per cases;
case
p44<>p;
then LSeg(p,p44) is_an_arc_of p,p44 by TOPREAL1:9;
then Segment(P,p1,p2,p,p44)=LSeg(p,p44) by A9,A5,A6,A7,A8,A11
,A13,A14,A23,A111,A114,Th25,SPRECT_4:4;
hence thesis by A4,A108,A110,A116,TOPREAL1:3;
end;
case
p44=p;
hence thesis by A4,A18,A108,A109,PARTFUN1:def 6;
end;
end;
hence thesis;
end;
LE p,p44,P,p1,p2 by A5,A6,A7,A8,A11,A13,A14,A23,A111,SPRECT_4:4;
hence thesis by A3,A4,A9,A108,A110,A113;
end;
case
A117: k<>0;
set p44=f/.(i+1);
A118: now
assume (f/.(i+1))`1<>e;
then for p9 being Point of TOP-REAL 2 st p9=f.(i+1+0) holds p9`1
<>e by A18,PARTFUN1:def 6;
hence contradiction by A27,A117;
end;
A119: LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A14,A15,TOPREAL1:def 3;
A120: now
assume not for p51 being Point of TOP-REAL 2 st LE p44,p51,P,p1
,p2 & LE p51,pk,P,p1,p2 holds p51`1>=e;
then consider p51 being Point of TOP-REAL 2 such that
A121: LE p44,p51,P,p1,p2 and
A122: LE p51,pk,P,p1,p2 and
A123: p51`1<e;
p51 in P by A121,JORDAN5C:def 3;
then consider Y3 being set such that
A124: p51 in Y3 and
A125: Y3 in { LSeg(f,i5) where i5 is Nat : 1 <= i5
& i5+1 <= len f } by A6,A10,TARSKI:def 4;
consider kk being Nat such that
A126: Y3=LSeg(f,kk) and
A127: 1 <= kk and
A128: kk+1 <= len f by A125;
A129: LE p51,f/.(kk+1),L~f,f/.1,f/.(len f) by A5,A124,A126,A127,A128,
JORDAN5C:26;
A130: LE f/.kk,p51,L~f,f/.1,f/.(len f) by A5,A124,A126,A127,A128,
JORDAN5C:25;
A131: kk-1>=0 by A127,XREAL_1:48;
A132: LSeg(f,kk)=LSeg(f/.kk,f/.(kk+1)) by A127,A128,TOPREAL1:def 3;
A133: kk<len f by A128,NAT_1:13;
then kk in Seg len f by A127,FINSEQ_1:1;
then
A134: kk in dom f by FINSEQ_1:def 3;
then
A135: f/.kk=f.kk by PARTFUN1:def 6;
A136: 1<kk+1 by A127,NAT_1:13;
then
A137: kk+1 in dom f by A128,FINSEQ_3:25;
f is one-to-one & kk<kk+1 by A5,NAT_1:13,TOPREAL1:def 8;
then
A138: f.kk <> f.(kk+1) by A134,A137,FUNCT_1:def 4;
now
per cases by A123,A124,A126,A132,Th3;
case
A139: (f/.(kk+1))`1<e;
set k2=kk-'i;
A140: LE p44,f/.(kk+1),L~f,f/.1,f/.(len f) by A6,A7,A8,A121,A129,
JORDAN5C:13;
now
assume kk-i<0;
then kk-i+i<0+i by XREAL_1:6;
then LE f/.(kk+1),f/.(i+1),L~f,f/.1,f/.(len f) by A5,A15,A136
,JORDAN5C:24,XREAL_1:7;
hence contradiction by A1,A6,A7,A8,A118,A139,A140,JORDAN5C:12
,TOPREAL4:2;
end;
then
A141: i+1+k2=1+i+(kk-i) by XREAL_0:def 2
.=kk+1;
A142: LSeg(f/.kk,f/.(kk+1)) c= L~f
proof
let z be object;
assume
A143: z in LSeg(f/.kk,f/.(kk+1));
LSeg(f/.kk,f/.(kk+1)) in { LSeg(f,i7) where i7 is
Nat : 1 <= i7 & i7+1 <= len f } by A127,A128,A132;
hence thesis by A10,A143,TARSKI:def 4;
end;
f is special by A5,TOPREAL1:def 8;
then
A144: (f/.kk)`1=(f/.(kk+1))`1 or (f/.kk)`2=(f/.(kk+1))`2 by A127,A128
,TOPREAL1:def 5;
f is one-to-one & kk<kk+1 by A5,NAT_1:13,TOPREAL1:def 8;
then
A145: f.kk <> f.(kk+1) by A134,A137,FUNCT_1:def 4;
A146: LE p51,f/.(i+1+k),L~f,f/.1,f/.(len f) by A6,A7,A8,A31,A122,
PARTFUN1:def 6;
A147: LE f/.(kk),f/.(i+1+k),L~f,f/.1,f/.(len f) by A6,A7,A8,A32,A122
,A130,JORDAN5C:13;
1<kk+1 by A127,NAT_1:13;
then P[k2] by A128,A139,A141,FINSEQ_4:15;
then k2>=k by A27;
then
A148: LE f/.(i+1+k),f/.(i+1+k2),L~f,f/.1,f/.(len f) by A5,A33,A128
,A141,JORDAN5C:24,XREAL_1:7;
f/.kk=f.kk & f/.(kk+1)=f.(kk+1) by A134,A137,PARTFUN1:def 6;
then LSeg(f/.kk,f/.(kk+1)) is_an_arc_of f/.kk,f/.(kk+1) by A145
,TOPREAL1:9;
then
A149: Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1 )) =LSeg(f/.
kk,f/.(kk+1)) by A9,A6,A7,A8,A141,A148,A147,A142,Th25,JORDAN5C:13;
Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1)) ={p8 where
p8 is Point of TOP-REAL 2: LE f/.kk,p8,L~f,f/.1,f/.(len f) & LE p8,f/.(kk+1),L~
f,f/.1,f/.(len f)} by JORDAN6:26;
then
A150: f/.(i+1+k) in Segment(L~f,f/.1,f/.(len f), f/.kk,f/.(kk
+1)) by A141,A148,A147;
then (f/.(kk))`1>e by A32,A108,A139,A149,Th2;
then (f/.kk)`1> (f/.(kk+1))`1 by A139,XXREAL_0:2;
then (f/.(i+1+k))`1<=p51`1 by A5,A124,A126,A127,A133,A132,A146
,A150,A149,A144,Th6;
hence contradiction by A32,A108,A123,XXREAL_0:2;
end;
case
A151: (f/.(kk))`1 <e & (f/.(kk+1))`1>=e;
set k2=kk-'(i+1);
A152: LSeg(f/.kk,f/.(kk+1)) c= L~f
proof
let z be object;
assume
A153: z in LSeg(f/.kk,f/.(kk+1));
LSeg(f/.kk,f/.(kk+1)) in { LSeg(f,i7) where i7 is
Nat : 1 <= i7 & i7+1 <= len f } by A127,A128,A132;
hence thesis by A10,A153,TARSKI:def 4;
end;
LE p51,f/.(kk+1),L~f,f/.1,f/.(len f) by A5,A124,A126,A127,A128,
JORDAN5C:26;
then
A154: LE p44,f/.(kk+1),L~f,f/.1,f/.(len f) by A6,A7,A8,A121,
JORDAN5C:13;
f/.(kk+1)=f.(kk+1) by A137,PARTFUN1:def 6;
then LSeg(f/.kk,f/.(kk+1)) is_an_arc_of f/.kk,f/.(kk+1) by A138
,A135,TOPREAL1:9;
then
A155: Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1)) ={p8 where
p8 is Point of TOP-REAL 2: LE f/.kk,p8,L~f,f/.1,f/.(len f) & LE p8,f/.(kk+1),L~
f,f/.1,f/.(len f)} & Segment(L~f,f/.1,f/.(len f),f/.kk,f/.(kk+1 )) =LSeg(f/.kk,
f/.(kk+1)) by A9,A5,A6,A7,A8,A127,A128,A152,Th25,JORDAN5C:23,JORDAN6:26;
A156: now
assume kk-(i+1)<0;
then kk-(i+1)+(i+1)<0+(i+1) by XREAL_1:6;
then kk<=i by NAT_1:13;
then
A157: LE f/.kk,f/.i,L~f,f/.1,f/.(len f) by A5,A23,A127,JORDAN5C:24;
A158: f/.i in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68;
LE f/.i,p44,L~f,f/.1,f/.(len f) by A5,A14,A15,JORDAN5C:23;
then LE f/.i,f/.(kk+1),L~f,f/.1,f/.(len f) by A154,
JORDAN5C:13;
then f/.i in LSeg(f/.kk,f/.(kk+1)) by A155,A157;
then LSeg(f/.kk,f/.(kk+1)) /\ LSeg(f/.i,f/.(i+1))<>{} by A158
,XBOOLE_0:def 4;
then
A159: not LSeg(f/.kk,f/.(kk+1)) misses LSeg (f/.i,f/.(i+1) )
by XBOOLE_0:def 7;
A160: kk-1=kk-'1 by A131,XREAL_0:def 2;
A161: now
assume
A162: i=kk-'1+2;
then kk+1<i+1 by A160,NAT_1:13;
then LE f/.(kk+1),p44,L~f,f/.1,f/.(len f) by A5,A15,A136,
JORDAN5C:24;
then p44=f/.(kk+1) by A1,A6,A7,A8,A154,JORDAN5C:12
,TOPREAL4:2;
then f.(i+1)=f/.(kk+1) by A18,PARTFUN1:def 6;
then
A163: f.(i+1)=f.(kk+1) by A137,PARTFUN1:def 6;
f is one-to-one by A5,TOPREAL1:def 8;
then i+1=kk+1 by A18,A137,A163,FUNCT_1:def 4;
hence contradiction by A160,A162;
end;
A164: f is s.n.c. by A5,TOPREAL1:def 8;
A165: LSeg(f,kk)=LSeg(f/.kk,f/.(kk+1)) & LSeg(f,i)=LSeg(f/.i
,f/.(i+1)) by A14,A15,A127,A128,TOPREAL1:def 3;
then i+1>=kk by A159,A164,TOPREAL1:def 7;
then
A166: i+1-1>=kk-1 by XREAL_1:9;
kk+1>=i by A159,A165,A164,TOPREAL1:def 7;
then
A167: i=kk-'1+0 or ... or i=kk-'1+2 by A160,A166,NAT_1:62;
A168: now
per cases by A160,A167,A161;
case
i=kk;
hence p44 in LSeg(f,kk) by A119,RLTOPSP1:68;
end;
case
i=kk-1;
hence p44 in LSeg(f,kk) by A132,RLTOPSP1:68;
end;
end;
f is special by A5,TOPREAL1:def 8;
then (f/.kk)`1=(f/.(kk+1))`1 or (f/.kk)`2=(f/.(kk+1))`2 by
A127,A128,TOPREAL1:def 5;
hence contradiction by A5,A6,A7,A8,A118,A121,A123,A124,A126
,A127,A133,A151,A168,Th7;
end;
then i+1+k2=i+1+(kk-(i+1)) by XREAL_0:def 2
.=kk;
then P[k2] by A127,A133,A151,FINSEQ_4:15;
then
A169: k2>=k by A27;
kk-'(i+1)=kk-(i+1) by A156,XREAL_0:def 2;
then kk-(i+1)+(i+1)>=k+(i+1) by A169,XREAL_1:7;
then
A170: LE f/.(i+1+k),f/.(kk),L~f,f/.1,f/.(len f) by A5,A30,A133,
JORDAN5C:24;
LE f/.(kk),f/.(i+1+k),L~f,f/.1,f/.(len f) by A6,A7,A8,A32,A122
,A130,JORDAN5C:13;
hence contradiction by A1,A6,A7,A8,A32,A108,A151,A170,
JORDAN5C:12,TOPREAL4:2;
end;
end;
hence contradiction;
end;
A171: p44 in LSeg(p,f/.(i+1)) by RLTOPSP1:68;
A172: for p5 being Point of TOP-REAL 2 st LE p,p5,P,p1,p2 & LE p5,
p44,P,p1,p2 holds p5`1>=e
proof
let p5 be Point of TOP-REAL 2;
A173: Segment(P,p1,p2,p,p44)={p8 where p8 is Point of TOP-REAL 2:
LE p,p8,P,p1,p2 & LE p8,p44,P,p1,p2} by JORDAN6:26;
assume LE p,p5,P,p1,p2 & LE p5,p44,P,p1,p2;
then
A174: p5 in Segment(P,p1,p2,p,p44) by A173;
p44 in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68;
then LSeg(p,p44) c= LSeg(f,i) by A11,A13,A119,TOPREAL1:6;
then
A175: LSeg(p,p44) c= P by A6,A19,A13;
now
per cases;
case
p44<>p;
then LSeg(p,p44) is_an_arc_of p,p44 by TOPREAL1:9;
then Segment(P,p1,p2,p,p44)=LSeg(p,p44) by A9,A5,A6,A7,A8,A11
,A13,A14,A23,A171,A175,Th25,SPRECT_4:4;
hence thesis by A4,A118,A174,TOPREAL1:3;
end;
case
p44=p;
then Segment(P,p1,p2,p,p44)={p44} by A1,A3,Th1,TOPREAL4:2;
hence thesis by A118,A174,TARSKI:def 1;
end;
end;
hence thesis;
end;
i+1<=i+1+k by NAT_1:11;
then
A176: LE p44,pk,P,p1,p2 by A5,A6,A7,A8,A17,A28,A32,JORDAN5C:24;
then
A177: p44 in P by JORDAN5C:def 3;
A178: for p5 being Point of TOP-REAL 2 st LE p5,pk,P,p1,p2 & LE p,p5
,P,p1,p2 holds p5`1>=e
proof
let p5 be Point of TOP-REAL 2;
assume that
A179: LE p5,pk,P,p1,p2 and
A180: LE p,p5,P,p1,p2;
A181: p5 in P by A179,JORDAN5C:def 3;
now
per cases by A1,A177,A181,Th19,TOPREAL4:2;
case
LE p44,p5,P,p1,p2;
hence thesis by A120,A179;
end;
case
LE p5,p44,P,p1,p2;
hence thesis by A172,A180;
end;
end;
hence thesis;
end;
LE p,p44,P,p1,p2 by A5,A6,A7,A8,A11,A13,A14,A23,A171,SPRECT_4:4;
then LE p,pk,P,p1,p2 by A176,JORDAN5C:13;
hence thesis by A3,A4,A9,A108,A178;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;