Copyright (c) 1997 Association of Mizar Users
environ
vocabulary ARYTM, PRE_TOPC, EUCLID, TOPMETR, PCOMPS_1, BORSUK_1, RCOMP_1,
ARYTM_3, ARYTM_1, RELAT_1, BOOLE, SUBSET_1, ORDINAL2, FUNCT_1, MCART_1,
FINSEQ_1, TOPREAL1, RELAT_2, TOPS_2, COMPTS_1, JORDAN5C, JORDAN3,
TREAL_1, SEQ_1, PSCOMP_1, TOPREAL2, SEQ_2, METRIC_1, SEQ_4, ABSVALUE,
SQUARE_1, FUNCT_5, JORDAN6;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, NAT_1, RCOMP_1, SETWOP_2, STRUCT_0, ABSVALUE, RELAT_1, FUNCT_1,
FUNCT_2, TOPREAL1, TOPREAL2, CONNSP_1, JORDAN2B, SQUARE_1, TSEP_1,
TOPMETR, PRE_TOPC, TOPS_2, COMPTS_1, BORSUK_1, EUCLID, METRIC_1,
PCOMPS_1, SEQ_4, JORDAN5C, TREAL_1, PSCOMP_1;
constructors RCOMP_1, ABSVALUE, TOPREAL2, CONNSP_1, JORDAN2B, TSEP_1, TOPS_2,
REAL_1, TOPREAL1, SQUARE_1, SETWOP_2, JORDAN5C, TREAL_1, PSCOMP_1, TSP_1,
COMPTS_1, YELLOW_8, PARTFUN1, MEMBERED;
clusters SUBSET_1, STRUCT_0, FUNCT_1, EUCLID, PRE_TOPC, TOPMETR, METRIC_1,
PSCOMP_1, BORSUK_2, TSEP_1, XREAL_0, RELSET_1, ARYTM_3, MEMBERED,
ZFMISC_1, ORDINAL2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, PRE_TOPC, JORDAN5C, XBOOLE_0;
theorems TARSKI, AXIOMS, RCOMP_1, TOPMETR, TOPS_1, METRIC_1, FUNCT_1, FUNCT_2,
SEQ_2, FINSEQ_1, REAL_1, ABSVALUE, SPPOL_1, REAL_2, SQUARE_1, PRE_TOPC,
TOPS_2, JORDAN1, JORDAN5B, JORDAN5C, TOPREAL1, STRUCT_0, TOPREAL5,
SUBSET_1, TREAL_1, PSCOMP_1, RELAT_1, TOPREAL2, JORDAN2B, ENUMSET1,
TOPREAL3, JORDAN5A, BORSUK_1, COMPTS_1, CONNSP_1, CONNSP_3, PCOMPS_1,
ZFMISC_1, TSEP_1, SEQ_4, RELSET_1, XREAL_0, SPRECT_1, XBOOLE_0, XBOOLE_1,
XCMPLX_1;
schemes DOMAIN_1, COMPLSP1;
begin :: Middle Points of Arcs
reserve x,y for set;
reserve s,r for real number;
reserve r1,r2 for Real;
reserve n for Nat;
reserve p,p3,q,q1,q2,q3 for Point of TOP-REAL 2;
canceled;
theorem Th2:
r<=s implies r <= (r+s)/2 & (r+s)/2 <= s
proof assume A1:r<=s;
per cases by A1,REAL_1:def 5;
suppose r<s;
hence thesis by TOPREAL3:3;
suppose r=s;
hence thesis by XCMPLX_1:65;
end;
theorem Th3: for TX being non empty TopSpace,
P being Subset of TX,
A being Subset of TX|P,
B being Subset of TX
st B is closed & A=B/\P holds A is closed
proof let TX be non empty TopSpace,P be Subset of TX,
A be Subset of TX|P,
B be Subset of TX;
assume A1: B is closed & A=B/\P;
[#](TX|P)=P by PRE_TOPC:def 10;
hence thesis by A1,PRE_TOPC:43;
end;
theorem Th4: for TX,TY being non empty TopSpace,
P being non empty Subset of TY,f being map of TX,TY|P
holds f is map of TX,TY &
for f2 being map of TX,TY
st f2=f & f is continuous holds f2 is continuous
proof let TX,TY be non empty TopSpace,
P be non empty Subset of TY,f be map of TX,TY|P;
A1: the carrier of TY|P = [#](TY|P) by PRE_TOPC:12 .=P by PRE_TOPC:def 10;
then f is Function of the carrier of TX,the carrier of TY
by FUNCT_2:9;
hence f is map of TX,TY ;
let f2 be map of TX,TY such that
A2: f2=f & f is continuous;
let P1 be Subset of TY;
assume A3:P1 is closed;
reconsider P3=P1/\P as Subset of TY|P by TOPS_2:38;
A4: P3 is closed by A3,Th3;
A5:f2"P=the carrier of TX by A1,A2,FUNCT_2:48
.=dom f2 by FUNCT_2:def 1;
f2"P1 c= dom f2 by RELAT_1:167;
then f2"P1=f2"P1 /\ f2"P by A5,XBOOLE_1:28
.=f"P3 by A2,FUNCT_1:137;
hence f2"P1 is closed by A2,A4,PRE_TOPC:def 12;
end;
theorem Th5:
for r being real number, P being Subset of TOP-REAL 2
st P={p where p is Point of TOP-REAL 2: p`1>=r} holds P is closed
proof let r be real number,P be Subset of TOP-REAL 2;
assume A1:P={p where p is Point of TOP-REAL 2: p`1>=r};
A2:1 in Seg 2 by FINSEQ_1:3;
A3:P`={p where p is Point of TOP-REAL 2: p`1<r}
proof
A4:P` c= {p where p is Point of TOP-REAL 2: p`1<r}
proof let x;assume A5: x in P`; then x in (the carrier of (TOP-REAL 2))
\ P
by SUBSET_1:def 5;
then A6:x in the carrier of (TOP-REAL 2) & not x in P by XBOOLE_0:def
4;
reconsider q=x as Point of TOP-REAL 2 by A5;
q`1<r by A1,A6;
hence x in {p where p is Point of TOP-REAL 2: p`1<r};
end;
{p where p is Point of TOP-REAL 2: p`1<r} c= P`
proof let x;assume x in {p where p is Point of TOP-REAL 2: p`1<r};
then consider p being Point of TOP-REAL 2 such that
A7:p=x & p`1<r;
now assume x in {q where q is Point of TOP-REAL 2: q`1>=r};
then consider q being Point of TOP-REAL 2 such that
A8:q=x & q`1>=r;
thus contradiction by A7,A8;
end;
then x in (the carrier of TOP-REAL 2) \P by A1,A7,XBOOLE_0:def 4;
hence x in P` by SUBSET_1:def 5;
end;
hence thesis by A4,XBOOLE_0:def 10;
end;
A9: P`={p where p is Point of TOP-REAL 2: r>Proj(p,1)}
proof
A10: P`c= {p where p is Point of TOP-REAL 2: r>Proj(p,1)}
proof let x;assume x in P`; then consider p being Point of TOP-REAL 2
such that A11:p=x & p`1<r by A3;
Proj(p,1)<r by A11,JORDAN2B:35;
hence thesis by A11;
end;
{p where p is Point of TOP-REAL 2: r>Proj(p,1)} c= P`
proof let x;assume x in
{p where p is Point of TOP-REAL 2: r>Proj(p,1)};
then consider q being Point of TOP-REAL 2 such that
A12:q=x & r>Proj(q,1);
q`1<r by A12,JORDAN2B:35;
hence x in P` by A3,A12;
end;
hence thesis by A10,XBOOLE_0:def 10;
end;
reconsider P1 = P` as Subset of TOP-REAL 2;
P1 is open by A2,A9,JORDAN2B:16;
hence P is closed by TOPS_1:29;
end;
theorem Th6:
for r being real number, P being Subset of TOP-REAL 2
st P={p where p is Point of TOP-REAL 2: p`1<=r} holds P is closed
proof let r be real number, P be Subset of TOP-REAL 2;
assume A1:P={p where p is Point of TOP-REAL 2: p`1<=r};
A2:1 in Seg 2 by FINSEQ_1:3;
A3:P`={p where p is Point of TOP-REAL 2: p`1>r}
proof
A4:P` c= {p where p is Point of TOP-REAL 2: p`1>r}
proof let x;assume A5: x in P`; then x in (the carrier of (TOP-REAL 2))
\ P
by SUBSET_1:def 5;
then A6:x in the carrier of (TOP-REAL 2) & not x in P by XBOOLE_0:def
4;
reconsider q=x as Point of TOP-REAL 2 by A5;
q`1>r by A1,A6;
hence x in {p where p is Point of TOP-REAL 2: p`1>r};
end;
{p where p is Point of TOP-REAL 2: p`1>r} c= P`
proof let x;assume x in {p where p is Point of TOP-REAL 2: p`1>r};
then consider p being Point of TOP-REAL 2 such that
A7:p=x & p`1>r;
now assume x in {q where q is Point of TOP-REAL 2: q`1<=r};
then consider q being Point of TOP-REAL 2 such that
A8:q=x & q`1<=r;
thus contradiction by A7,A8;
end;
then x in (the carrier of TOP-REAL 2) \P by A1,A7,XBOOLE_0:def 4;
hence x in P` by SUBSET_1:def 5;
end;
hence thesis by A4,XBOOLE_0:def 10;
end;
A9: P`={p where p is Point of TOP-REAL 2: r<Proj(p,1)}
proof
A10: P`c= {p where p is Point of TOP-REAL 2: r<Proj(p,1)}
proof let x;assume x in P`; then consider p being Point of TOP-REAL 2
such that A11:p=x & p`1>r by A3;
Proj(p,1)>r by A11,JORDAN2B:35;
hence thesis by A11;
end;
{p where p is Point of TOP-REAL 2: r<Proj(p,1)} c= P`
proof let x;assume x in
{p where p is Point of TOP-REAL 2: r<Proj(p,1)};
then consider q being Point of TOP-REAL 2 such that
A12:q=x & r<Proj(q,1);
q`1>r by A12,JORDAN2B:35;
hence x in P` by A3,A12;
end;
hence thesis by A10,XBOOLE_0:def 10;
end;
reconsider P1 = P` as Subset of TOP-REAL 2;
P1 is open by A2,A9,JORDAN2B:17;
hence P is closed by TOPS_1:29;
end;
theorem Th7:
for r being real number,P being Subset of TOP-REAL 2
st P={p where p is Point of TOP-REAL 2: p`1=r} holds P is closed
proof let r be real number,P be Subset of TOP-REAL 2;
assume A1:P={p where p is Point of TOP-REAL 2: p`1=r};
defpred P[Point of TOP-REAL 2] means $1`1>=r;
{p where p is Element of TOP-REAL 2 : P[p]}
is Subset of TOP-REAL 2 from SubsetD;
then reconsider P1={p where p is Point of TOP-REAL 2: p`1>=r}
as Subset of TOP-REAL 2;
A2:P1 is closed by Th5;
defpred Q[Point of TOP-REAL 2] means $1`1<=r;
{p where p is Element of TOP-REAL 2 : Q[p]}
is Subset of TOP-REAL 2 from SubsetD;
then reconsider P2={p where p is Point of TOP-REAL 2: p`1<=r}
as Subset of TOP-REAL 2;
A3:P2 is closed by Th6;
P=P1 /\ P2
proof
A4:P c= P1 /\ P2
proof let x;assume x in P;
then ex p being Point of TOP-REAL 2 st p=x & p`1=r by A1;
then x in P1 & x in P2;
hence x in P1 /\ P2 by XBOOLE_0:def 3;
end;
P1 /\ P2 c= P
proof let x;assume x in P1 /\ P2;
then A5:x in P1 & x in P2 by XBOOLE_0:def 3;
then consider q1 being Point of TOP-REAL 2 such that A6:q1=x & q1`1>=r;
consider q2 being Point of TOP-REAL 2 such that A7:q2=x & q2`1<=r by A5;
q1`1=r by A6,A7,AXIOMS:21;
hence x in P by A1,A6;
end;
hence thesis by A4,XBOOLE_0:def 10;
end;
hence P is closed by A2,A3,TOPS_1:35;
end;
theorem Th8:
for r being real number, P being Subset of TOP-REAL 2
st P={p where p is Point of TOP-REAL 2: p`2>=r} holds P is closed
proof let r be real number, P be Subset of TOP-REAL 2;
assume A1:P={p where p is Point of TOP-REAL 2: p`2>=r};
A2:2 in Seg 2 by FINSEQ_1:3;
A3:P`={p where p is Point of TOP-REAL 2: p`2<r}
proof
A4:P` c= {p where p is Point of TOP-REAL 2: p`2<r}
proof let x;assume A5: x in P`; then x in (the carrier of (TOP-REAL 2))
\ P
by SUBSET_1:def 5;
then A6:x in the carrier of (TOP-REAL 2) & not x in P by XBOOLE_0:def
4;
reconsider q=x as Point of TOP-REAL 2 by A5;
q`2<r by A1,A6;
hence x in {p where p is Point of TOP-REAL 2: p`2<r};
end;
{p where p is Point of TOP-REAL 2: p`2<r} c= P`
proof let x;assume x in {p where p is Point of TOP-REAL 2: p`2<r};
then consider p being Point of TOP-REAL 2 such that
A7:p=x & p`2<r;
now assume x in {q where q is Point of TOP-REAL 2: q`2>=r};
then consider q being Point of TOP-REAL 2 such that
A8:q=x & q`2>=r;
thus contradiction by A7,A8;
end;
then x in (the carrier of TOP-REAL 2) \P by A1,A7,XBOOLE_0:def 4;
hence x in P` by SUBSET_1:def 5;
end;
hence thesis by A4,XBOOLE_0:def 10;
end;
A9: P`={p where p is Point of TOP-REAL 2: r>Proj(p,2)}
proof
A10: P`c= {p where p is Point of TOP-REAL 2: r>Proj(p,2)}
proof let x;assume x in P`; then consider p being Point of TOP-REAL 2
such that A11:p=x & p`2<r by A3;
Proj(p,2)<r by A11,JORDAN2B:35;
hence thesis by A11;
end;
{p where p is Point of TOP-REAL 2: r>Proj(p,2)} c= P`
proof let x;assume x in
{p where p is Point of TOP-REAL 2: r>Proj(p,2)};
then consider q being Point of TOP-REAL 2 such that
A12:q=x & r>Proj(q,2);
q`2<r by A12,JORDAN2B:35;
hence x in P` by A3,A12;
end;
hence thesis by A10,XBOOLE_0:def 10;
end;
reconsider P1 = P` as Subset of TOP-REAL 2;
P1 is open by A2,A9,JORDAN2B:16;
hence P is closed by TOPS_1:29;
end;
theorem Th9:
for r being real number, P being Subset of TOP-REAL 2
st P={p where p is Point of TOP-REAL 2: p`2<=r} holds P is closed
proof let r be real number, P be Subset of TOP-REAL 2;
assume A1:P={p where p is Point of TOP-REAL 2: p`2<=r};
A2:2 in Seg 2 by FINSEQ_1:3;
A3:P`={p where p is Point of TOP-REAL 2: p`2>r}
proof
A4:P` c= {p where p is Point of TOP-REAL 2: p`2>r}
proof let x;assume A5: x in P`; then x in (the carrier of (TOP-REAL 2))
\ P
by SUBSET_1:def 5;
then A6:x in the carrier of (TOP-REAL 2) & not x in P by XBOOLE_0:def
4;
reconsider q=x as Point of TOP-REAL 2 by A5;
q`2>r by A1,A6;
hence x in {p where p is Point of TOP-REAL 2: p`2>r};
end;
{p where p is Point of TOP-REAL 2: p`2>r} c= P`
proof let x;assume x in {p where p is Point of TOP-REAL 2: p`2>r};
then consider p being Point of TOP-REAL 2 such that
A7:p=x & p`2>r;
now assume x in {q where q is Point of TOP-REAL 2: q`2<=r};
then consider q being Point of TOP-REAL 2 such that
A8:q=x & q`2<=r;
thus contradiction by A7,A8;
end;
then x in (the carrier of TOP-REAL 2) \P by A1,A7,XBOOLE_0:def 4;
hence x in P` by SUBSET_1:def 5;
end;
hence thesis by A4,XBOOLE_0:def 10;
end;
A9: P`={p where p is Point of TOP-REAL 2: r<Proj(p,2)}
proof
A10: P`c= {p where p is Point of TOP-REAL 2: r<Proj(p,2)}
proof let x;assume x in P`; then consider p being Point of TOP-REAL 2
such that A11:p=x & p`2>r by A3;
Proj(p,2)>r by A11,JORDAN2B:35;
hence thesis by A11;
end;
{p where p is Point of TOP-REAL 2: r<Proj(p,2)} c= P`
proof let x;assume x in
{p where p is Point of TOP-REAL 2: r<Proj(p,2)};
then consider q being Point of TOP-REAL 2 such that
A12:q=x & r<Proj(q,2);
q`2>r by A12,JORDAN2B:35;
hence x in P` by A3,A12;
end;
hence thesis by A10,XBOOLE_0:def 10;
end;
reconsider P1 = P` as Subset of TOP-REAL 2;
P1 is open by A2,A9,JORDAN2B:17;
hence P is closed by TOPS_1:29;
end;
theorem Th10:
for r being real number, P being Subset of TOP-REAL 2
st P={p where p is Point of TOP-REAL 2: p`2=r} holds P is closed
proof let r be real number, P be Subset of TOP-REAL 2;
assume A1:P={p where p is Point of TOP-REAL 2: p`2=r};
defpred P[Point of TOP-REAL 2] means $1`2>=r;
{p where p is Element of TOP-REAL 2 : P[p]}
is Subset of TOP-REAL 2 from SubsetD;
then reconsider P1={p where p is Point of TOP-REAL 2: p`2>=r}
as Subset of TOP-REAL 2;
A2:P1 is closed by Th8;
defpred Q[Point of TOP-REAL 2] means $1`2<=r;
{p where p is Element of TOP-REAL 2 : Q[p]}
is Subset of TOP-REAL 2 from SubsetD;
then reconsider P2={p where p is Point of TOP-REAL 2: p`2<=r}
as Subset of TOP-REAL 2;
A3:P2 is closed by Th9;
P=P1 /\ P2
proof
A4:P c= P1 /\ P2
proof let x;assume x in P;
then consider p being Point of TOP-REAL 2 such that A5:p=x & p`2=r by A1
;
x in P1 & x in P2 by A5;
hence x in P1 /\ P2 by XBOOLE_0:def 3;
end;
P1 /\ P2 c= P
proof let x;assume x in P1 /\ P2;
then A6:x in P1 & x in P2 by XBOOLE_0:def 3;
then consider q1 being Point of TOP-REAL 2 such that A7:q1=x & q1`2>=r;
consider q2 being Point of TOP-REAL 2 such that A8:q2=x & q2`2<=r by A6;
q1`2=r by A7,A8,AXIOMS:21;
hence x in P by A1,A7;
end;
hence thesis by A4,XBOOLE_0:def 10;
end;
hence P is closed by A2,A3,TOPS_1:35;
end;
theorem Th11:
for P being Subset of TOP-REAL n,
p1,p2 being Point of TOP-REAL n st
P is_an_arc_of p1,p2 holds P is connected
proof let P be Subset of TOP-REAL n,
p1,p2 be Point of TOP-REAL n;
assume
A1: P is_an_arc_of p1,p2;
then consider f being map of I[01], (TOP-REAL n)|P such that
A2: f is_homeomorphism & f.0 = p1 & f.1 = p2 by TOPREAL1:def 2;
reconsider P' = P as non empty Subset of TOP-REAL n by A1,TOPREAL1:4;
A3: f is continuous map of I[01],(TOP-REAL n)|P' by A2,TOPS_2:def 5;
A4: [#]I[01] is connected by CONNSP_1:28,TREAL_1:22;
A5:rng f=[#]((TOP-REAL n)|P) by A2,TOPS_2:def 5;
A6:[#]((TOP-REAL n)|P)=P by PRE_TOPC:def 10;
dom f=[#]I[01] by A2,TOPS_2:def 5;
then A7:P=f.:([#]I[01]) by A5,A6,RELAT_1:146;
f.:([#]I[01]) is connected by A3,A4,TOPREAL5:5;
hence P is connected by A7,CONNSP_3:34;
end;
theorem Th12:
for P being Subset of TOP-REAL 2,p1,p2
being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds P is closed
proof let P be Subset of TOP-REAL 2,p1,p2
be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2;
reconsider P00=P as Subset of TOP-REAL 2;
P00 is compact by A1,JORDAN5A:1;
hence P is closed by COMPTS_1:16;
end;
theorem Th13:
for P being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2
holds ex q being Point of TOP-REAL 2 st q in P & q `1 = (p1 `1+p2 `1)/2
proof let P be Subset of (TOP-REAL 2),
p1,p2 be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2;
then A2:p1 in P by TOPREAL1:4;
reconsider P' = P as non empty Subset of TOP-REAL 2
by A1,TOPREAL1:4;
consider f being map of I[01], (TOP-REAL 2)|P' such that
A3:f is_homeomorphism & f.0 = p1 & f.1 = p2 by A1,TOPREAL1:def 2;
A4:f is continuous by A3,TOPS_2:def 5;
consider h being map of TOP-REAL 2,R^1 such that
A5:for p being Element of TOP-REAL 2
holds h.p=Proj(p,1) by JORDAN2B:1;
1 in Seg 2 by FINSEQ_1:3;
then A6:h is continuous by A5,JORDAN2B:22;
A7: the carrier of (TOP-REAL 2)|P =
[#]((TOP-REAL 2)|P) by PRE_TOPC:12 .=P' by PRE_TOPC:def 10;
then A8:f is Function of the carrier of I[01],the carrier of TOP-REAL 2
by FUNCT_2:9;
then reconsider f1=f as map of I[01],TOP-REAL 2 ;
A9:f1 is continuous by A4,Th4;
h*f is Function of the carrier of I[01],the carrier of R^1
by A8,FUNCT_2:19;
then reconsider g= h*f as map of I[01],R^1 ;
A10:g is continuous by A6,A9,TOPS_2:58;
A11:dom f=[.0,1.] by BORSUK_1:83,FUNCT_2:def 1;
then A12:0 in dom f by TOPREAL5:1;
A13:1 in dom f by A11,TOPREAL5:1;
A14:g.0
=h.(f.0) by A12,FUNCT_1:23 .=Proj(p1,1) by A3,A5 .=p1`1 by JORDAN2B:35;
A15:g.1
=h.(f.1) by A13,FUNCT_1:23 .=Proj(p2,1) by A3,A5 .=p2`1 by JORDAN2B:35;
per cases;
suppose g.0<>g.1;
then consider r1 being Real such that
A16:0<r1 & r1<1 & g.r1=(p1`1+p2`1)/2
by A10,A14,A15,TOPREAL5:15;
A17:r1 in [.0,1.] by A16,TOPREAL5:1;
A18:r1 in the carrier of I[01] by A16,BORSUK_1:83,TOPREAL5:1;
then reconsider q1=f.r1 as Point of TOP-REAL 2 by A8,FUNCT_2:7;
A19:f.r1 in P by A7,A18,FUNCT_2:7;
g.r1= h.(f.r1) by A11,A17,FUNCT_1:23
.=Proj(q1,1) by A5 .=q1`1 by JORDAN2B:35;
hence thesis by A16,A19;
suppose g.0=g.1;
then p1 `1 = (p1 `1+p2 `1)/2 by A14,A15,XCMPLX_1:65;
hence thesis by A2;
end;
theorem Th14:
for P,Q being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 &
Q={q:q`1=(p1`1+p2`1)/2} holds P meets Q & P /\ Q is closed
proof
let P,Q be Subset of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
reconsider W = P as Subset of TOP-REAL 2;
assume A1:P is_an_arc_of p1,p2 & Q={q:q`1=(p1`1+p2`1)/2};
consider f being map of TOP-REAL 2,R^1 such that
A2: for p being Element of TOP-REAL 2
holds f.p=Proj(p,1) by JORDAN2B:1;
reconsider P' = P as non empty Subset of TOP-REAL 2
by A1,TOPREAL1:4;
1 in Seg 2 by FINSEQ_1:3;
then A3:f is continuous by A2,JORDAN2B:22;
A4:dom f=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
[#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 10;
then A5:the carrier of (TOP-REAL 2)|P'=P' by PRE_TOPC:12;
A6:dom (f|P)=(the carrier of TOP-REAL 2)/\P by A4,RELAT_1:90
.=P by XBOOLE_1:28;
rng (f|P) c= rng f by FUNCT_1:76;
then rng (f|P) c= the carrier of R^1 by XBOOLE_1:1;
then f|P is Function of the carrier of (TOP-REAL 2)|P,the carrier of R^1
by A5,A6,FUNCT_2:def 1,RELSET_1:11;
then reconsider g=f|P as map of (TOP-REAL 2)|P,R^1 ;
reconsider g as continuous map of (TOP-REAL 2)|P',R^1 by A3,TOPMETR:10;
A7:p1 in P & p2 in P by A1,TOPREAL1:4;
reconsider p1'=p1, p2'=p2 as Point of (TOP-REAL 2)|P by A1,A5,TOPREAL1:4;
A8:g.p1'=f.p1 by A7,FUNCT_1:72 .=Proj(p1,1) by A2
.=p1`1 by JORDAN2B:35;
A9: g.p2'=f.p2 by A7,FUNCT_1:72 .=Proj(p2,1) by A2
.=p2`1 by JORDAN2B:35;
W is connected by A1,Th11;
then A10:(TOP-REAL 2)|P is connected by CONNSP_1:def 3;
A11: now per cases;
case p1`1<=p2`1;
then p1`1<=(p1`1+p2`1)/2 & (p1`1+p2`1)/2<=p2`1 by Th2;
then consider xc being Point of (TOP-REAL 2)|P such that
A12:g.xc=(p1`1+p2`1)/2 by A8,A9,A10,TOPREAL5:10;
xc in P by A5;
then reconsider pc=xc as Point of TOP-REAL 2;
g.xc =f.xc by A5,FUNCT_1:72 .=Proj(pc,1) by A2 .=pc`1 by JORDAN2B:35;
then xc in Q by A1,A12;
hence P meets Q by A5,XBOOLE_0:3;
case p1`1>p2`1;
then p2`1<=(p1`1+p2`1)/2 & (p1`1+p2`1)/2<=p1`1
by Th2;
then consider xc being Point of (TOP-REAL 2)|P such that
A13:g.xc=(p1`1+p2`1)/2 by A8,A9,A10,TOPREAL5:10;
xc in P by A5;
then reconsider pc=xc as Point of TOP-REAL 2;
g.xc =f.xc by A5,FUNCT_1:72 .=Proj(pc,1) by A2 .=pc`1 by JORDAN2B:35;
then xc in Q by A1,A13;
hence P meets Q by A5,XBOOLE_0:3;
end;
reconsider P1 = P, Q1 = Q as Subset of TOP-REAL 2;
A14:P1 is closed by A1,Th12;
Q1 is closed by A1,Th7;
hence thesis by A11,A14,TOPS_1:35;
end;
theorem Th15:
for P,Q being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 &
Q={q:q`2=(p1`2+p2`2)/2} holds P meets Q & P /\ Q is closed
proof let P,Q1 be Subset of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
assume A1:P is_an_arc_of p1,p2 & Q1={q:q`2=(p1`2+p2`2)/2};
consider f being map of TOP-REAL 2,R^1 such that
A2: for p being Element of TOP-REAL 2
holds f.p=Proj(p,2) by JORDAN2B:1;
reconsider P' = P as non empty Subset of TOP-REAL 2
by A1,TOPREAL1:4;
2 in Seg 2 by FINSEQ_1:3;
then A3:f is continuous by A2,JORDAN2B:22;
A4:dom f=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
[#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 10;
then A5:the carrier of (TOP-REAL 2)|P'=P' by PRE_TOPC:12;
A6:dom (f|P)=(the carrier of TOP-REAL 2)/\P by A4,RELAT_1:90 .=P by
XBOOLE_1:28;
rng (f|P) c= rng f by FUNCT_1:76;
then rng (f|P) c= the carrier of R^1 by XBOOLE_1:1;
then f|P is Function of the carrier of (TOP-REAL 2)|P,the carrier of R^1
by A5,A6,FUNCT_2:def 1,RELSET_1:11;
then reconsider g=f|P as map of (TOP-REAL 2)|P,R^1 ;
reconsider g as continuous map of (TOP-REAL 2)|P',R^1 by A3,TOPMETR:10;
A7:p1 in P & p2 in P by A1,TOPREAL1:4;
reconsider p1'=p1, p2'=p2 as Point of (TOP-REAL 2)|P by A1,A5,TOPREAL1:4;
A8:g.p1'=f.p1 by A7,FUNCT_1:72 .=Proj(p1,2) by A2
.=p1`2 by JORDAN2B:35;
A9: g.p2'=f.p2 by A7,FUNCT_1:72 .=Proj(p2,2) by A2
.=p2`2 by JORDAN2B:35;
reconsider W = P as Subset of TOP-REAL 2;
W is connected by A1,Th11;
then A10:(TOP-REAL 2)|P is connected by CONNSP_1:def 3;
A11: now per cases;
case p1`2<=p2`2;
then p1`2<=(p1`2+p2`2)/2 & (p1`2+p2`2)/2<=p2`2
by Th2;
then consider xc being Point of (TOP-REAL 2)|P such that
A12:g.xc=(p1`2+p2`2)/2 by A8,A9,A10,TOPREAL5:10;
xc in P by A5;
then reconsider pc=xc as Point of TOP-REAL 2;
g.xc =f.xc by A5,FUNCT_1:72 .=Proj(pc,2) by A2 .=pc`2 by JORDAN2B:35;
then xc in Q1 by A1,A12;
hence P meets Q1 by A5,XBOOLE_0:3;
case p1`2>p2`2;
then p2`2<=(p1`2+p2`2)/2 & (p1`2+p2`2)/2<=p1`2
by Th2;
then consider xc being Point of (TOP-REAL 2)|P such that
A13:g.xc=(p1`2+p2`2)/2 by A8,A9,A10,TOPREAL5:10;
xc in P by A5;
then reconsider pc=xc as Point of TOP-REAL 2;
g.xc =f.xc by A5,FUNCT_1:72 .=Proj(pc,2) by A2 .=pc`2 by JORDAN2B:35;
then xc in Q1 by A1,A13;
hence P meets Q1 by A5,XBOOLE_0:3;
end;
reconsider P1 = P, Q2 = Q1 as Subset of TOP-REAL 2;
A14:P1 is closed by A1,Th12;
Q2 is closed by A1,Th10;
hence thesis by A11,A14,TOPS_1:35;
end;
definition let P be non empty Subset of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
func x_Middle(P,p1,p2) -> Point of TOP-REAL 2 means
:Def1: for Q being Subset of TOP-REAL 2 st
Q={q:q`1=(p1`1+p2`1)/2}
holds it=First_Point(P,p1,p2,Q);
existence
proof
{q:q`1=(p1`1+p2`1)/2} c= the carrier of TOP-REAL 2
proof let x;assume x in {q:q`1=(p1`1+p2`1)/2};
then consider q being Point of TOP-REAL 2 such that
A1:q=x & (q`1=(p1`1+p2`1)/2);
thus x in the carrier of TOP-REAL 2 by A1;
end;
then reconsider Q1={q:q`1=(p1`1+p2`1)/2}
as Subset of TOP-REAL 2;
reconsider q2=First_Point(P,p1,p2,Q1) as Point of TOP-REAL 2;
for Q being Subset of TOP-REAL 2
st Q={q:q`1=(p1`1+p2`1)/2}
holds q2=First_Point(P,p1,p2,Q);
hence thesis;
end;
uniqueness
proof let q3,q4 be Point of TOP-REAL 2;
assume A2:(for Q1 being Subset of TOP-REAL 2 st
Q1={q1:q1`1=(p1`1+p2`1)/2}
holds q3=First_Point(P,p1,p2,Q1)) &
(for Q2 being Subset of TOP-REAL 2 st
Q2={q2:q2`1=(p1`1+p2`1)/2}
holds q4=First_Point(P,p1,p2,Q2));
{q1:q1`1=(p1`1+p2`1)/2} c= the carrier of TOP-REAL 2
proof let x;assume x in {q1:q1`1=(p1`1+p2`1)/2};
then consider q being Point of TOP-REAL 2 such that
A3:q=x & (q`1=(p1`1+p2`1)/2);
thus x in the carrier of TOP-REAL 2 by A3;
end;
then reconsider Q3={q2:q2`1=(p1`1+p2`1)/2}
as Subset of TOP-REAL 2;
q3=First_Point(P,p1,p2,Q3) by A2;
hence q3=q4 by A2;
end;
end;
definition let P be non empty Subset of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
func y_Middle(P,p1,p2) -> Point of TOP-REAL 2 means
:Def2: for Q being Subset of TOP-REAL 2
st Q={q:q`2=(p1`2+p2`2)/2}
holds it=First_Point(P,p1,p2,Q);
existence
proof
{q:q`2=(p1`2+p2`2)/2} c= the carrier of TOP-REAL 2
proof let x;assume x in {q:q`2=(p1`2+p2`2)/2};
then consider q being Point of TOP-REAL 2 such that
A1:q=x & (q`2=(p1`2+p2`2)/2);
thus x in the carrier of TOP-REAL 2 by A1;
end;
then reconsider Q1={q:q`2=(p1`2+p2`2)/2}
as Subset of TOP-REAL 2;
reconsider q2=First_Point(P,p1,p2,Q1) as Point of TOP-REAL 2;
for Q being Subset of TOP-REAL 2
st Q={q:q`2=(p1`2+p2`2)/2}
holds q2=First_Point(P,p1,p2,Q);
hence thesis;
end;
uniqueness
proof let q3,q4 be Point of TOP-REAL 2;
assume A2:(for Q1 being Subset of TOP-REAL 2 st
Q1={q1:q1`2=(p1`2+p2`2)/2}
holds q3=First_Point(P,p1,p2,Q1)) &
(for Q2 being Subset of TOP-REAL 2 st
Q2={q2:q2`2=(p1`2+p2`2)/2}
holds q4=First_Point(P,p1,p2,Q2));
{q1:q1`2=(p1`2+p2`2)/2} c= the carrier of TOP-REAL 2
proof let x;assume x in {q1:q1`2=(p1`2+p2`2)/2};
then consider q being Point of TOP-REAL 2 such that
A3:q=x & (q`2=(p1`2+p2`2)/2);
thus x in the carrier of TOP-REAL 2 by A3;
end;
then reconsider Q3={q2:q2`2=(p1`2+p2`2)/2}
as Subset of TOP-REAL 2;
q3=First_Point(P,p1,p2,Q3) by A2;
hence q3=q4 by A2;
end;
end;
theorem
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
x_Middle(P,p1,p2) in P & y_Middle(P,p1,p2) in P
proof let P be non empty Subset of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2;
deffunc F(Point of TOP-REAL 2)=$1;
defpred P[Point of TOP-REAL 2] means $1`1=(p1`1+p2`1)/2;
reconsider Q={F(q):P[q]} as Subset of TOP-REAL 2
from SubsetFD;
A2:x_Middle(P,p1,p2)=First_Point(P,p1,p2,Q) by Def1;
P meets Q & P /\ Q is closed by A1,Th14;
then A3: x_Middle(P,p1,p2) in P /\ Q by A1,A2,JORDAN5C:def 1;
defpred Q[Point of TOP-REAL 2] means $1`2=(p1`2+p2`2)/2;
reconsider Q2={F(q):Q[q]} as Subset of TOP-REAL 2
from SubsetFD;
A4: y_Middle(P,p1,p2)=First_Point(P,p1,p2,Q2) by Def2;
P meets Q2 & P /\ Q2 is closed by A1,Th15;
then y_Middle(P,p1,p2) in P /\ Q2 by A1,A4,JORDAN5C:def 1;
hence thesis by A3,XBOOLE_0:def 3;
end;
theorem
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
p1=x_Middle(P,p1,p2) iff p1`1=p2`1
proof let P be non empty Subset of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2;
A2:now assume A3:p1=x_Middle(P,p1,p2);
deffunc F(Point of TOP-REAL 2)=$1;
defpred P[Point of TOP-REAL 2] means $1`1=(p1`1+p2`1)/2;
reconsider Q1={F(q):P[q]} as Subset of TOP-REAL 2
from SubsetFD;
A4:P meets Q1 & P /\ Q1 is closed by A1,Th14;
x_Middle(P,p1,p2)=First_Point(P,p1,p2,Q1) by Def1;
then p1 in P /\ Q1 by A1,A3,A4,JORDAN5C:def 1;
then p1 in Q1 by XBOOLE_0:def 3;
then ex q st q=p1 & q`1=(p1`1+p2`1)/2;
hence p1`1=p2`1 by XCMPLX_1:67;
end;
now assume p1`1=p2`1;
then A5:p1`1=(p1`1+p2`1)/2 by XCMPLX_1:65;
for Q being Subset of TOP-REAL 2 st
Q={q:q`1=(p1`1+p2`1)/2}
holds p1=First_Point(P,p1,p2,Q)
proof let Q be Subset of TOP-REAL 2;
assume A6: Q={q:q`1=(p1`1+p2`1)/2};
then A7:p1 in Q by A5;
P meets Q & P /\ Q is closed by A1,A6,Th14;
hence p1=First_Point(P,p1,p2,Q) by A1,A7,JORDAN5C:3;
end;
hence p1=x_Middle(P,p1,p2) by Def1;
end;
hence thesis by A2;
end;
theorem
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
p1=y_Middle(P,p1,p2) iff p1`2=p2`2
proof let P be non empty Subset of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2;
A2:now assume A3:p1=y_Middle(P,p1,p2);
deffunc F(Point of TOP-REAL 2)=$1;
defpred P[Point of TOP-REAL 2] means $1`2=(p1`2+p2`2)/2;
reconsider Q1={F(q):P[q]} as Subset of TOP-REAL 2
from SubsetFD;
A4:P meets Q1 & P /\ Q1 is closed by A1,Th15;
y_Middle(P,p1,p2)=First_Point(P,p1,p2,Q1) by Def2;
then p1 in P /\ Q1 by A1,A3,A4,JORDAN5C:def 1;
then p1 in Q1 by XBOOLE_0:def 3;
then consider q such that A5:q=p1 & q`2=(p1`2+p2`2)/2;
thus p1`2=p2`2 by A5,XCMPLX_1:67;
end;
now assume p1`2=p2`2;
then A6:p1`2=(p1`2+p2`2)/2 by XCMPLX_1:65;
for Q being Subset of TOP-REAL 2 st
Q={q:q`2=(p1`2+p2`2)/2}
holds p1=First_Point(P,p1,p2,Q)
proof let Q be Subset of TOP-REAL 2;
assume A7: Q={q:q`2=(p1`2+p2`2)/2};
then A8:p1 in Q by A6;
P meets Q & P /\ Q is closed by A1,A7,Th15;
hence p1=First_Point(P,p1,p2,Q) by A1,A8,JORDAN5C:3;
end;
hence p1=y_Middle(P,p1,p2) by Def2;
end;
hence thesis by A2;
end;
begin ::Segments of Arcs
theorem Th19:
for P being Subset of TOP-REAL 2,
p1,p2,q1,q2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2
& LE q1,q2,P,p1,p2 holds LE q2,q1,P,p2,p1
proof let P be Subset of TOP-REAL 2,
p1,p2,q1,q2 be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2;
hence q2 in P & q1 in P by JORDAN5C:def 3;
reconsider P' = P as non empty Subset of TOP-REAL 2
by A1,TOPREAL1:4;
let f be map of I[01], (TOP-REAL 2)|P, s1, s2 be Real;
assume A2:f is_homeomorphism
& f.0 = p2 & f.1 = p1
& f.s1 = q2 & 0 <= s1 & s1 <= 1
& f.s2 = q1 & 0 <= s2 & s2 <= 1;
then A3: 1-0>=1-s1 by REAL_1:92;
A4: 1-0>=1-s2 by A2,REAL_1:92;
A5: 1-1<=1-s1 by A2,REAL_1:92;
A6: 1-1<=1-s2 by A2,REAL_1:92;
set Ex = L[01]((0,1)(#),(#)(0,1));
A7: Ex is_homeomorphism by TREAL_1:21;
set g = f * Ex;
A8: Ex.(0,1)(#) = 0 by BORSUK_1:def 17,TREAL_1:8,12;
A9: Ex.(#)(0,1) = 1 by BORSUK_1:def 18,TREAL_1:8,12;
dom f = [#]I[01] by A2,TOPS_2:def 5;
then A10: rng Ex = dom f by A7,TOPMETR:27,TOPS_2:def 5;
then A11: dom g = dom Ex by RELAT_1:46;
rng g = rng f by A10,RELAT_1:47;
then A12: rng g = [#] ((TOP-REAL 2) | P) by A2,TOPS_2:def 5;
dom g = [#]I[01] by A7,A11,TOPMETR:27,TOPS_2:def 5;
then A13: dom g = the carrier of I[01]
& rng g = the carrier of ((TOP-REAL 2) | P) by A12,PRE_TOPC:12;
then g is
Function of the carrier of I[01], the carrier of ((TOP-REAL 2)|P')
by FUNCT_2:def 1,RELSET_1:11;
then reconsider g as map of I[01], (TOP-REAL 2)|P' ;
A14: g is_homeomorphism by A2,A7,TOPMETR:27,TOPS_2:71;
A15:(1-s1) in dom g & (1-s2) in dom g by A3,A4,A5,A6,A13,JORDAN5A:2;
A16: g.0 = p1 by A2,A9,A13,BORSUK_1:def 17,FUNCT_1:22,TREAL_1:8;
A17: g.1 = p2 by A2,A8,A13,BORSUK_1:def 18,FUNCT_1:22,TREAL_1:8;
reconsider qs1=1-s1,qs2=1-s2 as Point of Closed-Interval-TSpace(0,1)
by A3,A4,A5,A6,JORDAN5A:2,TOPMETR:27;
A18: Ex.qs1 = (1-(1-s1))*1+(1-s1)*0
by BORSUK_1:def 17,def 18,TREAL_1:8,def 3
.=s1 by XCMPLX_1:18;
A19: Ex.qs2 = (1-(1-s2))*1+(1-s2)*0
by BORSUK_1:def 17,def 18,TREAL_1:8,def 3
.=s2 by XCMPLX_1:18;
A20: g.(1-s1) = q2 by A2,A15,A18,FUNCT_1:22;
g.(1-s2) = q1 by A2,A15,A19,FUNCT_1:22;
then 1-s2<=1-s1 by A1,A3,A4,A5,A6,A14,A16,A17,A20,JORDAN5C:def 3;
then s1<=1-(1-s2) by REAL_2:165;
hence s1<=s2 by XCMPLX_1:18;
end;
definition let P be Subset of TOP-REAL 2,
p1,p2,q1 be Point of TOP-REAL 2;
func L_Segment(P,p1,p2,q1) -> Subset of TOP-REAL 2 equals
:Def3: {q : LE q,q1,P,p1,p2};
coherence
proof
{q : LE q,q1,P,p1,p2} c= the carrier of TOP-REAL 2
proof let x;assume x in {q : LE q,q1,P,p1,p2};
then consider q such that A1:q=x & LE q,q1,P,p1,p2;
thus x in the carrier of TOP-REAL 2 by A1;
end;
hence {q : LE q,q1,P,p1,p2} is Subset of TOP-REAL 2;
end;
end;
definition let P be Subset of TOP-REAL 2,
p1,p2,q1 be Point of TOP-REAL 2;
func R_Segment(P,p1,p2,q1) -> Subset of TOP-REAL 2 equals
:Def4: {q: LE q1,q,P,p1,p2};
coherence
proof
{q : LE q1,q,P,p1,p2} c= the carrier of TOP-REAL 2
proof let x;assume x in {q : LE q1,q,P,p1,p2};
then consider q such that A1:q=x & LE q1,q,P,p1,p2;
thus x in the carrier of TOP-REAL 2 by A1;
end;
hence {q : LE q1,q,P,p1,p2} is Subset of TOP-REAL 2;
end;
end;
theorem Th20:
for P being Subset of TOP-REAL 2,
p1,p2,q1 being Point of TOP-REAL 2
holds L_Segment(P,p1,p2,q1) c= P
proof let P be Subset of TOP-REAL 2,
p1,p2,q1 be Point of TOP-REAL 2;
let x;assume x in L_Segment(P,p1,p2,q1);
then x in {q: LE q,q1,P,p1,p2} by Def3;
then ex q st q=x & LE q,q1,P,p1,p2;
hence x in P by JORDAN5C:def 3;
end;
theorem Th21:
for P being Subset of TOP-REAL 2,
p1,p2,q1 being Point of TOP-REAL 2
holds R_Segment(P,p1,p2,q1) c= P
proof let P be Subset of TOP-REAL 2,
p1,p2,q1 be Point of TOP-REAL 2;
let x;assume x in R_Segment(P,p1,p2,q1);
then x in {q: LE q1,q,P,p1,p2} by Def4;
then ex q st q=x & LE q1,q,P,p1,p2;
hence x in P by JORDAN5C:def 3;
end;
theorem
for P being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
L_Segment(P,p1,p2,p1)={p1}
proof let P be Subset of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2;
then A2:p1 in P by TOPREAL1:4;
thus L_Segment(P,p1,p2,p1) c= {p1}
proof let x;assume x in L_Segment(P,p1,p2,p1);
then x in {q: LE q,p1,P,p1,p2} by Def3;
then consider q such that A3:q=x & LE q,p1,P,p1,p2;
q in P by A3,JORDAN5C:def 3;
then LE p1,q,P,p1,p2 & LE q,p2,P,p1,p2 by A1,JORDAN5C:10;
then q=p1 by A1,A3,JORDAN5C:12;
hence x in {p1} by A3,TARSKI:def 1;
end;
let x;assume x in {p1};
then A4:x=p1 by TARSKI:def 1;
LE p1,p1,P,p1,p2 by A1,A2,JORDAN5C:9;
then x in {q: LE q,p1,P,p1,p2} by A4;
hence x in L_Segment(P,p1,p2,p1) by Def3;
end;
canceled 2;
theorem
for P being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
L_Segment(P,p1,p2,p2)=P
proof let P be Subset of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
assume A1:P is_an_arc_of p1,p2;
thus L_Segment(P,p1,p2,p2) c= P by Th20;
let x;assume A2:x in P;
then reconsider p=x as Point of TOP-REAL 2;
LE p,p2,P,p1,p2 by A1,A2,JORDAN5C:10;
then x in {q: LE q,p2,P,p1,p2};
hence x in L_Segment(P,p1,p2,p2) by Def3;
end;
theorem
for P being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
R_Segment(P,p1,p2,p2)={p2}
proof let P be Subset of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2;
then A2:p2 in P by TOPREAL1:4;
thus R_Segment(P,p1,p2,p2) c= {p2}
proof let x;assume x in R_Segment(P,p1,p2,p2);
then x in {q: LE p2,q,P,p1,p2} by Def4;
then consider q such that A3:q=x & LE p2,q,P,p1,p2;
q in P by A3,JORDAN5C:def 3;
then LE p1,q,P,p1,p2 & LE q,p2,P,p1,p2 by A1,JORDAN5C:10;
then q=p2 by A1,A3,JORDAN5C:12;
hence x in {p2} by A3,TARSKI:def 1;
end;
let x;assume x in {p2};
then A4:x=p2 by TARSKI:def 1;
LE p2,p2,P,p1,p2 by A1,A2,JORDAN5C:9;
then x in {q: LE p2,q,P,p1,p2} by A4;
hence x in R_Segment(P,p1,p2,p2) by Def4;
end;
theorem
for P being Subset of TOP-REAL 2,p1,p2 being
Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
R_Segment(P,p1,p2,p1)=P
proof let P be Subset of TOP-REAL 2,
p1,p2 be Point of TOP-REAL 2;
assume A1:P is_an_arc_of p1,p2;
thus R_Segment(P,p1,p2,p1) c= P by Th21;
let x;assume A2:x in P;
then reconsider p=x as Point of TOP-REAL 2;
LE p1,p,P,p1,p2 by A1,A2,JORDAN5C:10;
then x in {q: LE p1,q,P,p1,p2};
hence x in R_Segment(P,p1,p2,p1) by Def4;
end;
theorem
for P being 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 holds
R_Segment(P,p1,p2,q1)=L_Segment(P,p2,p1,q1)
proof let P be Subset of TOP-REAL 2,
p1,p2,q1 be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2 & q1 in P;
then A2:P is_an_arc_of p2,p1 by JORDAN5B:14;
A3:R_Segment(P,p1,p2,q1)=
{q: LE q1,q,P,p1,p2} by Def4;
A4:L_Segment(P,p2,p1,q1)=
{q : LE q,q1,P,p2,p1} by Def3;
A5: {q: LE q1,q,P,p1,p2} c= {q2 : LE q2,q1,P,p2,p1}
proof let x;assume x in {q: LE q1,q,P,p1,p2};
then consider q such that A6:q=x & LE q1,q,P,p1,p2;
LE q,q1,P,p2,p1 by A1,A6,Th19;
hence x in {q2 : LE q2,q1,P,p2,p1} by A6;
end;
{q2 : LE q2,q1,P,p2,p1} c= {q: LE q1,q,P,p1,p2}
proof let x;assume x in {q: LE q,q1,P,p2,p1};
then consider q such that A7:q=x & LE q,q1,P,p2,p1;
LE q1,q,P,p1,p2 by A2,A7,Th19;
hence x in {q2 : LE q1,q2,P,p1,p2} by A7;
end;
hence thesis by A3,A4,A5,XBOOLE_0:def 10;
end;
definition let P be Subset of TOP-REAL 2,
p1,p2,q1,q2 be Point of TOP-REAL 2;
func Segment(P,p1,p2,q1,q2) -> Subset of TOP-REAL 2 equals
:Def5: R_Segment(P,p1,p2,q1) /\ L_Segment(P,p1,p2,q2);
correctness;
end;
theorem
for P being Subset of TOP-REAL 2,
p1,p2,q1,q2 being Point of TOP-REAL 2
holds Segment(P,p1,p2,q1,q2)={q:LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2}
proof let P be Subset of TOP-REAL 2,
p1,p2,q1,q2 be Point of TOP-REAL 2;
thus Segment(P,p1,p2,q1,q2) c= {q:LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2}
proof let x;assume x in Segment(P,p1,p2,q1,q2);
then x in R_Segment(P,p1,p2,q1) /\ L_Segment(P,p1,p2,q2) by Def5;
then A1:x in R_Segment(P,p1,p2,q1) & x in L_Segment(P,p1,p2,q2)
by XBOOLE_0:def 3;
then x in {q: LE q1,q,P,p1,p2} by Def4;
then consider q such that A2:q=x & (LE q1,q,P,p1,p2);
x in {p: LE p,q2,P,p1,p2} by A1,Def3;
then consider p such that A3: p=x & (LE p,q2,P,p1,p2);
thus x in {p3:LE q1,p3,P,p1,p2 & LE p3,q2,P,p1,p2} by A2,A3;
end;
let x;assume x in {q:LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2};
then consider q such that A4: q=x & (LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2)
;
x in {q3: LE q1,q3,P,p1,p2} by A4;
then A5:x in R_Segment(P,p1,p2,q1) by Def4;
x in {q3: LE q3,q2,P,p1,p2} by A4;
then x in L_Segment(P,p1,p2,q2) by Def3;
then x in R_Segment(P,p1,p2,q1) /\ L_Segment(P,p1,p2,q2) by A5,XBOOLE_0
:def 3;
hence x in Segment(P,p1,p2,q1,q2) by Def5;
end;
theorem Th30:
for P being Subset of TOP-REAL 2,
p1,p2,q1,q2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2
holds LE q1,q2,P,p1,p2 iff LE q2,q1,P,p2,p1
proof let P be Subset of TOP-REAL 2,
p1,p2,q1,q2 be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2;
then P is_an_arc_of p2,p1 by JORDAN5B:14;
hence thesis by A1,Th19;
end;
theorem Th31: for P being Subset of TOP-REAL 2,
p1,p2,q being Point of TOP-REAL 2 st
P is_an_arc_of p1,p2 & q in P
holds L_Segment(P,p1,p2,q)=R_Segment(P,p2,p1,q)
proof let P be Subset of TOP-REAL 2,
p1,p2,q be Point of TOP-REAL 2;
assume A1:P is_an_arc_of p1,p2 & q in P;
thus L_Segment(P,p1,p2,q) c= R_Segment(P,p2,p1,q)
proof let x;assume
x in L_Segment(P,p1,p2,q);
then x in {p: LE p,q,P,p1,p2} by Def3;
then consider p such that A2: p=x & (LE p,q,P,p1,p2);
LE q,p,P,p2,p1 by A1,A2,Th30;
then x in {q1: LE q,q1,P,p2,p1} by A2;
hence x in R_Segment(P,p2,p1,q) by Def4;
end;
let x;assume
x in R_Segment(P,p2,p1,q);
then x in {p: LE q,p,P,p2,p1} by Def4;
then consider p such that A3: p=x & (LE q,p,P,p2,p1);
LE p,q,P,p1,p2 by A1,A3,Th30;
then x in {q1: LE q1,q,P,p1,p2} by A3;
hence x in L_Segment(P,p1,p2,q) by Def3;
end;
theorem
for P being 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 Segment(P,p1,p2,q1,q2)=Segment(P,p2,p1,q2,q1)
proof let P be Subset of TOP-REAL 2,
p1,p2,q1,q2 be Point of TOP-REAL 2;
assume A1:P is_an_arc_of p1,p2 & q1 in P & q2 in P;
A2:Segment(P,p1,p2,q1,q2)=R_Segment(P,p1,p2,q1)/\ L_Segment(P,p1,p2,q2)
by Def5;
A3:L_Segment(P,p1,p2,q2)=R_Segment(P,p2,p1,q2) by A1,Th31;
P is_an_arc_of p2,p1 by A1,JORDAN5B:14;
then R_Segment(P,p1,p2,q1)=L_Segment(P,p2,p1,q1) by A1,Th31;
hence thesis by A2,A3,Def5;
end;
begin ::Decomposition of a Simple Closed Curve into Two Arcs
definition let s be real number;
func Vertical_Line(s) -> Subset of TOP-REAL 2 equals
:Def6: {p where p is Point of TOP-REAL 2: p`1=s};
correctness
proof
{p where p is Point of TOP-REAL 2: p`1=s} c= the carrier of (TOP-REAL 2)
proof let x;assume x in {p where p is Point of TOP-REAL 2: p`1=s};
then ex p being Point of TOP-REAL 2 st p=x & p`1=s;
hence x in the carrier of (TOP-REAL 2);
end;
hence thesis;
end;
func Horizontal_Line(s) -> Subset of TOP-REAL 2 equals
:Def7: {p: p`2=s};
correctness
proof
{p where p is Point of TOP-REAL 2: p`2=s} c= the carrier of (TOP-REAL 2)
proof let x;assume x in {p where p is Point of TOP-REAL 2: p`2=s};
then ex p being Point of TOP-REAL 2 st p=x & p`2=s;
hence x in the carrier of (TOP-REAL 2);
end;
hence thesis;
end;
end;
theorem Th33:for r being real number holds
Vertical_Line(r) is closed & Horizontal_Line(r) is closed
proof let r be real number;
A1: Vertical_Line(r)={p where p is Point of TOP-REAL 2: p`1=r} by Def6;
Horizontal_Line(r)={p where p is Point of TOP-REAL 2: p`2=r} by Def7;
hence thesis by A1,Th7,Th10;
end;
theorem Th34:
for r being real number,p being Point of TOP-REAL 2 holds
p in Vertical_Line(r) iff p`1=r
proof let r be real number,p be Point of TOP-REAL 2;
hereby assume p in Vertical_Line(r);
then p in {q where q is Point of TOP-REAL 2: q`1=r} by Def6;
then ex q being Point of TOP-REAL 2 st q=p & q`1=r;
hence p`1=r;
end;
assume p`1 = r;
then p in {p1 where p1 is Point of TOP-REAL 2: p1`1=r};
hence thesis by Def6;
end;
theorem
for r being real number,p being Point of TOP-REAL 2 holds
p in Horizontal_Line(r) iff p`2=r
proof let r be real number,p be Point of TOP-REAL 2;
hereby assume p in Horizontal_Line(r);
then p in {q where q is Point of TOP-REAL 2: q`2=r} by Def7;
then ex q being Point of TOP-REAL 2 st q=p & q`2=r;
hence p`2=r;
end;
assume p`2 = r;
then p in {p1 where p1 is Point of TOP-REAL 2: p1`2=r};
hence thesis by Def7;
end;
canceled 4;
theorem Th40: for P being compact non empty Subset of TOP-REAL 2
st P is_simple_closed_curve
ex P1,P2 being non empty Subset of TOP-REAL 2 st
P1 is_an_arc_of W-min(P),E-max(P)
& P2 is_an_arc_of E-max(P),W-min(P)
& P1 /\ P2={W-min(P),E-max(P)}
& P1 \/ P2=P
& First_Point(P1,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(P2,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2
proof let P be compact non empty Subset of TOP-REAL 2;
assume A1:P is_simple_closed_curve;
A2:W-min(P) in P & E-max(P) in P by SPRECT_1:15,16;
W-min(P)<>E-max(P) by A1,TOPREAL5:25;
then consider P01,P02 being non empty Subset of TOP-REAL
2
such that
A3:P01 is_an_arc_of W-min(P),E-max(P)
& P02 is_an_arc_of W-min(P),E-max(P) &
P = P01 \/ P02 & P01 /\ P02 = {W-min(P),E-max(P)} by A1,A2,TOPREAL2:5;
reconsider P01,P02 as non empty Subset of TOP-REAL 2;
A4:P01 is_an_arc_of E-max(P),W-min(P) by A3,JORDAN5B:14;
A5:P02 is_an_arc_of E-max(P),W-min(P) by A3,JORDAN5B:14;
reconsider P001=P01, P002=P02 as non empty Subset of TOP-REAL 2;
A6:(E-max P)`1 = E-bound P by PSCOMP_1:104;
A7:Vertical_Line((W-bound(P)+E-bound(P))/2) is closed by Th33;
P01 is closed by A3,Th12;
then A8:P01/\Vertical_Line((W-bound(P)+E-bound(P))/2) is closed
by A7,TOPS_1:35;
A9:Vertical_Line((W-bound(P)+E-bound(P))/2) is closed by Th33;
P02 is closed by A3,Th12;
then A10:P02/\Vertical_Line((W-bound(P)+E-bound(P))/2) is closed
by A9,TOPS_1:35;
consider q1 being Point of TOP-REAL 2 such that
A11: q1 in P001 & q1`1 = ((W-min(P))`1+(E-max(P))`1)/2 by A3,Th13;
A12:(W-min P)`1 = W-bound P by PSCOMP_1:84;
(E-max P)`1 = E-bound P by PSCOMP_1:104;
then q1 in {p where p is Point of TOP-REAL 2: p`1=(W-bound(P)+E-bound(P
))/2}
by A11,A12;
then q1 in Vertical_Line((W-bound(P)+E-bound(P))/2) by Def6;
then P01/\Vertical_Line((W-bound(P)+E-bound(P))/2) <> {}
by A11,XBOOLE_0:def 3;
then A13:P01 meets Vertical_Line((W-bound(P)+E-bound(P))/2) by XBOOLE_0:
def 7;
consider q2 being Point of TOP-REAL 2 such that
A14: q2 in P002 & q2`1 = ((W-min(P))`1+(E-max(P))`1)/2 by A3,Th13;
q2 in {p where p is Point of TOP-REAL 2: p`1=(W-bound(P)+E-bound(P))/2
}
by A6,A12,A14;
then q2 in Vertical_Line((W-bound(P)+E-bound(P))/2) by Def6;
then P02/\Vertical_Line((W-bound(P)+E-bound(P))/2) <> {}
by A14,XBOOLE_0:def 3;
then A15:P02 meets Vertical_Line((W-bound(P)+E-bound(P))/2) by XBOOLE_0:
def 7
;
per cases;
suppose
First_Point(P01,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(P02,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2;
hence thesis by A3,A5;
suppose
A16:First_Point(P01,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2<=
Last_Point(P02,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2;
now per cases by A16,REAL_1:def 5;
case
A17:First_Point(P01,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2<
Last_Point(P02,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2;
A18:First_Point(P01,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2)) =
Last_Point(P01,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2)) by A3,A8,A13,JORDAN5C:18;
Last_Point(P02,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))
= First_Point(P02,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))
by A3,A10,A15,JORDAN5C:18;
hence
ex P1,P2 being non empty Subset of TOP-REAL 2 st
P1 is_an_arc_of W-min(P),E-max(P)
& P2 is_an_arc_of E-max(P),W-min(P)
& P1 /\ P2={W-min(P),E-max(P)}
& P1 \/ P2=P
& First_Point(P1,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(P2,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2
by A3,A4,A17,A18;
case
A19:First_Point(P01,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2=
Last_Point(P02,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2;
set p=First_Point(P01,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2));
set p'=Last_Point(P02,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2));
A20:W-bound(P)<E-bound(P) by A1,TOPREAL5:23;
A21:p in P01/\ Vertical_Line((W-bound(P)+E-bound(P))/2)
by A3,A8,A13,JORDAN5C:def 1;
then A22:p in P01 by XBOOLE_0:def 3;
p in Vertical_Line((W-bound(P)+E-bound(P))/2) by A21,XBOOLE_0:def 3
;
then A23:p`1=(W-bound(P)+E-bound(P))/2 by Th34;
A24:p' in P02/\ Vertical_Line((W-bound(P)+E-bound(P))/2)
by A5,A10,A15,JORDAN5C:def 2;
then A25:p' in P02 by XBOOLE_0:def 3;
p' in Vertical_Line((W-bound(P)+E-bound(P))/2) by A24,XBOOLE_0:def
3
;
then p'`1=(W-bound(P)+E-bound(P))/2 by Th34;
then p=p' by A19,A23,TOPREAL3:11;
then p in P01 /\ P02 by A22,A25,XBOOLE_0:def 3;
then p=W-min(P) or p=E-max(P) by A3,TARSKI:def 2;
hence contradiction by A6,A12,A20,A23,XCMPLX_1:67;
end;
then consider P1,P2 being non empty Subset of TOP-REAL 2
such that
A26: P1 is_an_arc_of W-min(P),E-max(P)
& P2 is_an_arc_of E-max(P),W-min(P)
& P1 /\ P2={W-min(P),E-max(P)}
& P1 \/ P2=P
& First_Point(P1,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(P2,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2;
reconsider P1,P2 as non empty Subset of TOP-REAL 2;
take P1, P2;
thus thesis by A26;
end;
begin ::Uniqueness of Decomposition of a Simple Closed Curve
theorem Th41:for P being Subset of I[01] st
P=(the carrier of I[01]) \{0,1} holds P is open
proof let P be Subset of I[01];
assume A1:P=(the carrier of I[01]) \{0,1};
A2:0 in [.0,1.] by TOPREAL5:1;
A3:1 in [.0,1.] by TOPREAL5:1;
{0} is Subset of I[01] by A2,BORSUK_1:83,ZFMISC_1:37;
then reconsider Q0={0} as Subset of I[01];
A4:Q0 is closed by A2,BORSUK_1:83,PCOMPS_1:10;
{1} is Subset of I[01] by A3,BORSUK_1:83,ZFMISC_1:37;
then reconsider Q1={1} as Subset of I[01];
Q1 is closed by A3,BORSUK_1:83,PCOMPS_1:10;
then A5:Q0 \/ Q1 is closed by A4,TOPS_1:36;
A6:Q0 \/ Q1={0,1} by ENUMSET1:41;
[#](I[01])\(Q0 \/ Q1) is open by A5,PRE_TOPC:def 6;
hence P is open by A1,A6,PRE_TOPC:12;
end;
canceled 2;
theorem Th44:for r,s being real number holds ].r,s.[ misses {r,s}
proof let r,s be real number;
assume A1: ].r,s.[ /\{r,s}<>{};
consider x being Element of ].r,s.[ /\ {r,s};
A2:x in ].r,s.[ & x in {r,s} by A1,XBOOLE_0:def 3;
then reconsider r1=x as Real;
r1 in {s1 where s1 is Real :r<s1 & s1<s} by A2,RCOMP_1:def 2;
then consider s1 being Real such that A3:s1=r1 & (r<s1 & s1<s);
thus contradiction by A2,A3,TARSKI:def 2;
end;
theorem Th45: for a,b,c being real number holds c in ].a,b.[ iff a < c & c < b
proof
let a,b,c be real number;
A1: c is Real by XREAL_0:def 1;
A2:now assume c in ].a,b.[;
then c in {r where r is Real:a<r & r<b} by RCOMP_1:def 2;
then consider r being Real such that A3: r=c & (a<r & r<b);
thus a<c & c <b by A3;
end;
now assume a < c & c < b;
then c in {r where r is Real:a<r & r<b} by A1;
hence c in ].a,b.[ by RCOMP_1:def 2;
end;
hence thesis by A2;
end;
theorem
for P being Subset of R^1, r,s being real number st
P=].r,s.[ holds P is open
proof let P be Subset of R^1, r,s be real number;
assume A1: P=].r,s.[;
{r1:r<r1} c= REAL
proof let x;assume x in {r1:r<r1};
then consider r1 such that A2:r1=x & r<r1;
thus x in REAL by A2;
end;
then reconsider P1={r1 where r1 is Real:r<r1} as Subset of R^1
by TOPMETR:24;
{r2:s>r2} c= REAL
proof let x;assume x in {r2:s>r2};
then consider r2 such that A3:r2=x & s>r2;
thus x in REAL by A3;
end;
then reconsider P2={r2 where r2 is Real:s>r2} as Subset of R^1
by TOPMETR:24;
A4:P1 is open by TOPREAL5:7;
A5:P2 is open by TOPREAL5:8;
P=P1 /\ P2
proof
A6:P c= P1 /\ P2
proof let x;assume A7:x in P;
then reconsider r1=x as Real by TOPMETR:24;
A8:r<r1 & r1<s by A1,A7,Th45;
then A9:x in P1;
x in P2 by A8;
hence x in P1 /\ P2 by A9,XBOOLE_0:def 3;
end;
P1 /\ P2 c= P
proof let x;assume x in P1 /\ P2;
then A10:x in P1 & x in P2 by XBOOLE_0:def 3;
then consider r1 such that A11:r1=x & r<r1;
consider r2 such that A12:r2=x & s>r2 by A10;
thus x in P by A1,A11,A12,Th45;
end;
hence thesis by A6,XBOOLE_0:def 10;
end;
hence P is open by A4,A5,TOPS_1:38;
end;
theorem Th47: for S being non empty TopSpace,
P1,P2 being Subset of S,
P1' being Subset of S|P2 st P1=P1' & P1 c= P2
holds S|P1=(S|P2)|P1'
proof let S be non empty TopSpace,
P1,P2 be Subset of S,
P1' be Subset of S|P2;
assume A1:P1=P1' & P1 c= P2;
A2:[#](S|P2)=P2 by PRE_TOPC:def 10;
[#](S|P2)=P2 by PRE_TOPC:def 10;
then A3:the carrier of (S|P2)=P2 by PRE_TOPC:12;
A4:[#]((S|P2)|P1')=P1 by A1,PRE_TOPC:def 10;
P1 c= the carrier of S;
then A5:[#]((S|P2)|P1') c= [#](S) by A4,PRE_TOPC:12;
for R being Subset of (S|P2)|P1' holds
R in the topology of (S|P2)|P1' iff
ex Q being Subset of S st
Q in the topology of S & R=Q/\[#]((S|P2)|P1')
proof let R be Subset of (S|P2)|P1';
A6:now assume R in the topology of (S|P2)|P1';
then consider Q0 being Subset of S|P2 such that
A7: Q0 in the topology of S|P2 & R=Q0/\[#]((S|P2)|P1')
by PRE_TOPC:def 9;
consider Q1 being Subset of S such that
A8: Q1 in the topology of S & Q0=Q1/\[#](S|P2) by A7,PRE_TOPC:def 9;
R=Q1/\(P2/\P1) by A2,A4,A7,A8,XBOOLE_1:16
.=Q1/\[#]((S|P2)|P1') by A1,A4,XBOOLE_1:28;
hence ex Q being Subset of S st
Q in the topology of S & R=Q/\[#]((S|P2)|P1') by A8;
end;
now given Q being Subset of S such that
A9:Q in the topology of S & R=Q/\[#]((S|P2)|P1');
reconsider R'=Q/\[#](S|P2) as Subset of S|P2
by A2,A3,XBOOLE_1:17;
A10:R' in the topology of (S|P2) by A9,PRE_TOPC:def 9;
R'/\[#]((S|P2)|P1')=Q/\(P2/\P1) by A2,A4,XBOOLE_1:16
.=R by A1,A4,A9,XBOOLE_1:28;
hence R in the topology of (S|P2)|P1' by A10,PRE_TOPC:def 9;
end;
hence R in the topology of (S|P2)|P1' iff
ex Q being Subset of S st
Q in the topology of S & R=Q/\[#]((S|P2)|P1') by A6;
end;
then (S|P2)|P1' is SubSpace of S by A5,PRE_TOPC:def 9;
hence S|P1=(S|P2)|P1' by A4,PRE_TOPC:def 10;
end;
theorem Th48:for P7 being Subset of I[01] st
P7=(the carrier of I[01]) \{0,1} holds P7<>{} & P7 is connected
proof let P7 be Subset of I[01];
assume A1: P7=(the carrier of I[01]) \{0,1};
A2:1/2 in [.0,1.] by TOPREAL5:1;
A3: not 1/2 in {0,1} by TARSKI:def 2;
then A4:1/2 in [.0,1.]\{0,1} by A2,XBOOLE_0:def 4;
A5:[#](I[01]|P7)=P7 by PRE_TOPC:def 10;
then A6:the carrier of I[01]|P7=P7 by PRE_TOPC:12;
for A,B being Subset of I[01]|P7
st [#](I[01]|P7) = A \/ B & A <> {}(I[01]|P7)
& B <> {}(I[01]|P7) & A is open &
B is open holds A meets B
proof
let A,B be Subset of I[01]|P7;
assume that A7: [#](I[01]|P7) = A \/ B and
A8: A <> {}(I[01]|P7) & B <> {}(I[01]|P7) and
A9: A is open and A10: B is open;
assume A11: A misses B;
A12: ].0,1.[ misses {0,1} by Th44;
A13:P7=(].0,1.[ \/ {0,1})\{0,1} by A1,BORSUK_1:83,RCOMP_1:11
.=].0,1.[ \{0,1} by XBOOLE_1:40 .=].0,1.[ by A12,XBOOLE_1:83;
reconsider D1=[.0,1.] as Subset of R^1 by TOPMETR:24;
reconsider P1=P7 as Subset of R^1 by A13,TOPMETR:24;
I[01]=R^1|D1 by TOPMETR:26,27;
then A14: I[01]|P7=R^1|P1 by Th47,BORSUK_1:83;
P1={r1:0<r1 & r1<1} by A13,RCOMP_1:def 2;
then P1 is open by JORDAN2B:32;
then A15: I[01]|P7 is non empty open SubSpace of R^1
by A1,A4,A6,A14,BORSUK_1:83,STRUCT_0:def 1,TSEP_1:16;
reconsider P = A, Q = B as non empty Subset of REAL
by A6,A8,A13,XBOOLE_1:1;
the carrier of RealSpace = the carrier of TopSpaceMetr(RealSpace)
by TOPMETR:16;
then reconsider A0 = P, B0 = Q as non empty Subset of R^1
by METRIC_1:def 14,TOPMETR:def 7;
A16: A0 is open & B0 is open by A9,A10,A15,TSEP_1:17;
consider xp being Element of P;
reconsider xp as Real;
A17: xp in P;
A18: P is bounded_below
proof
now
take p = 0;
let r be real number;
assume r in P;
then r in ].0,1.[ by A6,A13;
then r in {w where w is Real : 0<w & w<1} by RCOMP_1:def 2;
then ex u being Real st u = r & 0<u & u<1;
hence p <= r;
end;
hence thesis by SEQ_4:def 2;
end;
A19: Q is bounded_below
proof
now
take p = 0;
let r be real number;
assume r in Q;
then r in ].0,1.[ by A6,A13;
then r in {w where w is Real : 0<w & w<1} by RCOMP_1:def 2;
then ex u being Real st u = r & 0<u & u<1;
hence p <= r;
end;
hence thesis by SEQ_4:def 2;
end;
reconsider l = lower_bound Q as Element of REAL by XREAL_0:def 1;
reconsider m = l as Point of RealSpace by METRIC_1:def 14;
reconsider t = m as Point of R^1 by TOPMETR:16,def 7;
A20: not l in Q
proof
assume l in Q;
then consider s being real number such that
A21: s > 0 and A22: Ball(m,s) c= B0 by A16,TOPMETR:22,def 7;
reconsider s as Element of REAL by XREAL_0:def 1;
reconsider e1 = l-s/2
as Point of RealSpace by METRIC_1:def 14;
A23:l-(l-s/2)=s/2 by XCMPLX_1:18;
A24:s/2>0 by A21,REAL_2:127;
s/2<s by A21,SEQ_2:4;
then abs(l - (l-s/2)) < s by A23,A24,ABSVALUE:def 1;
then (the distance of RealSpace).(m,e1) < s
by METRIC_1:def 13,def 14;
then dist(m,e1) < s by METRIC_1:def 1;
then e1 in {z where z is Element of
RealSpace : dist(m,z)<s};
then l-s/2 in Ball(m,s) by METRIC_1:18;
then l<=l-s/2 by A19,A22,SEQ_4:def 5; then l+s/2<=l by REAL_1:
84;
then l+s/2-l<=l-l by REAL_1:49; then s/2<=l-l by XCMPLX_1:26;
then s/2<=0 by XCMPLX_1:14;
hence contradiction by A21,REAL_2:127;
end;
A25: now assume A26:l<=0;
0<xp & xp<1 by A6,A13,A17,Th45;
then xp-l>0 by A26,SQUARE_1:11;
then consider r5 being real number such that
A27: (r5 in Q & r5<l+(xp-l)) by A19,SEQ_4:def 5;
reconsider r5 as Real by XREAL_0:def 1;
A28:r5<xp by A27,XCMPLX_1:27;
A29:{s5 where s5 is Real:s5 in P & r5<s5} c= P
proof let y be set;
assume y in {s5 where s5 is Real:s5 in P & r5<s5};
then ex s5 being Real st s5=y & s5 in P & r5<s5;
hence y in P;
end;
then reconsider P5={s5 where s5 is Real:s5 in P & r5<s5}
as Subset of REAL by XBOOLE_1:1;
A30:xp in P5 by A28;
A31: P5 is bounded_below by A18,A29,RCOMP_1:3;
reconsider l5 = lower_bound P5 as Real by XREAL_0:def 1;
reconsider m5 = l5 as Point of RealSpace by METRIC_1:def 14;
A32: now assume A33:l5<=r5;
now assume l5<r5; then r5-l5>0 by SQUARE_1:11;
then consider r be real number such that
A34: r in P5 & r<l5+(r5-l5) by A30,A31,SEQ_4:def 5;
consider s6 being Real such that
A35:s6=r & s6 in P & r5<s6 by A34;
thus contradiction by A34,A35,XCMPLX_1:27;
end;
then l5=r5 by A33,AXIOMS:21;
then consider r7 being real number such that
A36: r7 > 0 and A37: Ball(m5,r7) c= B0
by A16,A27,TOPMETR:22,def 7;
consider r9 being real number such that
A38: r9 in P5 & r9<l5+r7 by A30,A31,A36,SEQ_4:def 5;
reconsider r9 as Real by XREAL_0:def 1;
reconsider e8=r9
as Point of RealSpace by METRIC_1:def 14;
l5<=r9 by A31,A38,SEQ_4:def 5;
then A39:r9-l5>=0 by SQUARE_1:12;
r9-l5<l5+r7-l5 by A38,REAL_1:54;
then r9-l5<r7 by XCMPLX_1:26;
then abs(r9 - l5) < r7 by A39,ABSVALUE:def 1;
then (the distance of RealSpace).(e8,m5) < r7
by METRIC_1:def 13,def 14;
then dist(e8,m5) < r7 by METRIC_1:def 1;
then e8 in {z where z is Element of
RealSpace : dist(m5,z)<r7};
then e8 in Ball(m5,r7) by METRIC_1:18;
hence contradiction by A11,A29,A37,A38,XBOOLE_0:3;
end;
0<r5 & r5<1 by A6,A13,A27,Th45;
then A40:l5>0 by A32,AXIOMS:22;
A41:l5-r5>0 by A32,SQUARE_1:11;
consider q being Element of P5;
A42:q in P5 by A30;
then reconsider q1=q as Real;
q1 in P by A29,A42;
then A43:0<q1 & q1<1 by A6,A13,Th45;
l5<=q1 by A30,A31,SEQ_4:def 5;
then l5<1 by A43,AXIOMS:22;
then l5 in ].0,1.[ by A40,Th45;
then A44:l5 in P or l5 in Q by A5,A7,A13,XBOOLE_0:def 2;
now assume l5 in P;
then consider s5 being real number such that
A45: s5 > 0 and A46: Ball(m5,s5) c= P
by A16,TOPMETR:22,def 7;
reconsider s5 as Element of REAL by XREAL_0:def 1;
set s5'=min(s5,l5-r5);
A47:s5'>0 by A41,A45,SPPOL_1:13;
then A48:s5'/2>0 by REAL_2:127;
A49:s5'<=s5 by SQUARE_1:35;
A50:s5'/2<s5' by A47,SEQ_2:4;
s5'<=l5-r5 by SQUARE_1:35;
then s5'/2<l5-r5 by A50,AXIOMS:22;
then s5'/2+r5<l5-r5+r5 by REAL_1:53;
then s5'/2+r5<l5 by XCMPLX_1:27;
then s5'/2+r5-s5'/2<l5-s5'/2 by REAL_1:54;
then A51:r5<l5-s5'/2 by XCMPLX_1:26;
reconsider e1 = l5-s5'/2
as Point of RealSpace by METRIC_1:def 14;
A52:l5-(l5-s5'/2)=s5'/2 by XCMPLX_1:18;
s5'/2<s5' by A47,SEQ_2:4;
then s5'/2<s5 by A49,AXIOMS:22;
then abs(l5 - (l5-s5'/2)) < s5 by A48,A52,ABSVALUE:def 1;
then (real_dist).(l5,l5-s5'/2) < s5 by METRIC_1:def 13;
then dist(m5,e1) < s5 by METRIC_1:def 1,def 14;
then e1 in {z where z is Element of
RealSpace : dist(m5,z)<s5};
then l5-s5'/2 in Ball(m5,s5) by METRIC_1:18;
then l5-s5'/2 in {s7 where s7 is Real:s7 in P & r5<s7}
by A46,A51;
then A53:l5<=l5-s5'/2 by A31,SEQ_4:def 5;
s5'/2>0 by A47,REAL_2:127;
then l5<l5+s5'/2 by REAL_1:69;
then l5-s5'/2<l5+s5'/2-s5'/2 by REAL_1:54;
hence contradiction by A53,XCMPLX_1:26;
end;
then consider s1 being real number such that
A54: s1 > 0 and A55: Ball(m5,s1) c= B0
by A16,A44,TOPMETR:22,def 7;
s1/2>0 by A54,REAL_2:127;
then consider r2 be real number such that
A56:(r2 in P5 & r2<l5+s1/2) by A30,A31,SEQ_4:def 5;
reconsider r2 as Real by XREAL_0:def 1;
A57:l5<=r2 by A31,A56,SEQ_4:def 5;
reconsider s3 = r2-l5 as Real;
reconsider e1 = l5+s3
as Point of RealSpace by METRIC_1:def 14;
A58:r2-l5>=0 by A57,SQUARE_1:12;
A59:l5+s3-l5=s3 by XCMPLX_1:26;
r2-l5<l5+s1/2-l5 by A56,REAL_1:92;
then A60:s3<s1/2 by XCMPLX_1:26;
s1/2<s1 by A54,SEQ_2:4;
then A61:l5+s3-l5<s1 by A59,A60,AXIOMS:22;
abs(l5+s3 - l5)=l5+s3-l5 by A58,A59,ABSVALUE:def 1;
then (real_dist).(l5+s3,l5) < s1 by A61,METRIC_1:def 13;
then dist(e1,m5) < s1 by METRIC_1:def 1,def 14;
then l5+s3 in {z where z is Element of
RealSpace : dist(m5,z)<s1};
then l5+s3 in Ball(m5,s1) & l5+s3 in P5
by A56,METRIC_1:18,XCMPLX_1:27;
then A62:l5+s3 in P5 /\ Q by A55,XBOOLE_0:def 3;
P5 /\ Q c= P /\ Q by A29,XBOOLE_1:26;
hence contradiction by A11,A62,XBOOLE_0:def 7;
end;consider q being Element of Q;
A63:q in Q;
reconsider q1=q as Real;
A64:0<q1 & q1<1 by A6,A13,A63,Th45;
l<=q1 by A19,SEQ_4:def 5;
then l<1 by A64,AXIOMS:22;
then l in ].0,1.[ by A25,Th45;
then t in A0 & A0 is open by A5,A7,A9,A13,A15,A20,TSEP_1:17,
XBOOLE_0:def 2;
then consider s1 being real number such that
A65: s1 > 0 and A66: Ball(m,s1) c= A0 by TOPMETR:22,def 7;
s1/2>0 by A65,REAL_2:127;
then consider r2 be real number such that
A67: r2 in Q & r2<l+s1/2 by A19,SEQ_4:def 5;
reconsider r2 as Real by XREAL_0:def 1;
A68:l<=r2 by A19,A67,SEQ_4:def 5;
set s3=r2-l;
reconsider e1 = l+s3 as Point of RealSpace by METRIC_1:def 14;
A69:r2-l>=0 by A68,SQUARE_1:12;
A70:l+s3-l=s3 by XCMPLX_1:26;
r2-l<l+s1/2-l by A67,REAL_1:92;
then A71:s3<s1/2 by XCMPLX_1:26;
s1/2<s1 by A65,SEQ_2:4;
then A72:l+s3-l<s1 by A70,A71,AXIOMS:22;
abs(l+s3 - l)=l+s3-l by A69,A70,ABSVALUE:def 1;
then (real_dist).(l+s3,l) < s1 by A72,METRIC_1:def 13;
then dist(e1,m) < s1 by METRIC_1:def 1,def 14;
then l+s3 in {z where z is Element of
RealSpace : dist(m,z)<s1};
then l+s3 in Ball(m,s1) & l+s3 in Q by A67,METRIC_1:18,XCMPLX_1:27
;
hence contradiction by A11,A66,XBOOLE_0:3;
end;
then I[01]|P7 is connected by CONNSP_1:12;
hence thesis by A1,A2,A3,BORSUK_1:83,CONNSP_1:def 3,XBOOLE_0:def 4;
end;
theorem Th49:for P being Subset of TOP-REAL n,
p1,p2 being Point of TOP-REAL n st P is_an_arc_of p1,p2
holds p1<>p2
proof let P be Subset of TOP-REAL n,
p1,p2 be Point of TOP-REAL n;
assume P is_an_arc_of p1,p2;
then consider f being map of I[01], (TOP-REAL n)|P such that
A1:f is_homeomorphism & f.0 = p1 & f.1 = p2 by TOPREAL1:def 2;
1 in [.0,1.] by TOPREAL5:1;
then 1 in [#](I[01]) by BORSUK_1:83,PRE_TOPC:12;
then A2:1 in dom f by A1,TOPS_2:def 5;
A3:f is one-to-one by A1,TOPS_2:def 5;
0 in [.0,1.] by TOPREAL5:1;
then 0 in [#](I[01]) by BORSUK_1:83,PRE_TOPC:12;
then 0 in dom f by A1,TOPS_2:def 5;
hence thesis by A1,A2,A3,FUNCT_1:def 8;
end;
theorem
for P being Subset of TOP-REAL n,
Q being Subset of (TOP-REAL n)|P,
p1,p2 being Point of TOP-REAL n st
P is_an_arc_of p1,p2 & Q=P\{p1,p2} holds Q is open
proof let P be Subset of TOP-REAL n,
Q be Subset of (TOP-REAL n)|P,
p1,p2 be Point of TOP-REAL n;
assume A1:P is_an_arc_of p1,p2 & Q=P\{p1,p2};
then reconsider P' = P as non empty Subset of TOP-REAL n
by TOPREAL1:4;
consider f being map of I[01], (TOP-REAL n)|P' such that
A2:f is_homeomorphism & f.0 = p1 & f.1 = p2 by A1,TOPREAL1:def 2;
reconsider f1=f as Function;
A3:f" is_homeomorphism by A2,TOPS_2:70;
reconsider g=f" as map of (TOP-REAL n)|P,I[01];
reconsider g1=g as Function;
(the carrier of I[01])\{0,1} is Subset of I[01] by XBOOLE_1:
36
;
then reconsider R=(the carrier of I[01])\{0,1}
as Subset of I[01];
A4:R is open by Th41;
A5:f is one-to-one by A2,TOPS_2:def 5;
A6:g is one-to-one by A3,TOPS_2:def 5;
A7:g is continuous by A2,TOPS_2:def 5;
A8:[#](I[01])=dom f by A2,TOPS_2:def 5;
0 in [.0,1.] by TOPREAL5:1;
then 0 in [#](I[01]) by BORSUK_1:83,PRE_TOPC:12;
then A9:0 in dom f by A2,TOPS_2:def 5;
1 in the carrier of I[01] by BORSUK_1:83,TOPREAL5:1;
then 1 in [#](I[01]) by PRE_TOPC:12;
then A10:1 in dom f by A2,TOPS_2:def 5;
rng f=[#]((TOP-REAL n)|P) by A2,TOPS_2:def 5;
then A11:f""=f by A5,TOPS_2:64;
rng g= [#](I[01]) by A3,TOPS_2:def 5;
then A12: g1" =f1 by A6,A11,TOPS_2:def 4;
g"(R)=g1"(the carrier of I[01])\g1"({0,1}) by FUNCT_1:138
.=((g1").:(the carrier of I[01]))\g1"({0,1}) by A6,FUNCT_1:155
.=f1.:(the carrier of I[01])\ (g1").:({0,1}) by A6,A12,FUNCT_1:155
.=f1.:([#](I[01]))\ f1.:({0,1}) by A12,PRE_TOPC:12
.=rng f\ f.:({0,1}) by A8,RELAT_1:146
.=[#]((TOP-REAL n)|P)\ f.:({0,1}) by A2,TOPS_2:def 5
.=P\ f.:({0,1}) by PRE_TOPC:def 10
.=Q by A1,A2,A9,A10,FUNCT_1:118;
hence thesis by A4,A7,TOPS_2:55;
end;
::A proof of the following is almost same as JORDAN5A:1.
canceled;
theorem Th52:
for P being Subset of TOP-REAL n,
P1,P2 being non empty Subset of TOP-REAL n,
Q being Subset of (TOP-REAL n)|P,
p1,p2 being Point of TOP-REAL n st p1 in P & p2 in P &
P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2
& P1 \/ P2 = P & P1 /\ P2={p1,p2} & Q=P1\{p1,p2}
holds Q is open
proof let P be Subset of TOP-REAL n,
P1,P2 be non empty Subset of TOP-REAL n,
Q be Subset of (TOP-REAL n)|P,
p1,p2 be Point of TOP-REAL n;
assume A1: p1 in P & p2 in P &
P1 is_an_arc_of p1,p2 &
P2 is_an_arc_of p1,p2 &
P1 \/ P2 = P & P1 /\ P2={p1,p2} & Q=P1\{p1,p2};
reconsider P21=P2 as Subset of TOP-REAL n;
A2: P21 is compact by A1,JORDAN5A:1;
p1 in P1 /\ P2 by A1,TARSKI:def 2;
then A3:p1 in P1 & p1 in P2 by XBOOLE_0:def 3;
A4:[#]((TOP-REAL n)|P)=P by PRE_TOPC:def 10;
then A5:the carrier of (TOP-REAL n)|P=P by PRE_TOPC:12;
A6:(TOP-REAL n)|P is non empty by A1,A4,STRUCT_0:def 1;
P2 c= P by A1,XBOOLE_1:7;
then reconsider P2'=P21 as Subset of (TOP-REAL n)|P by A5;
p2 in P1 /\ P2 by A1,TARSKI:def 2;
then A7:p2 in P1 & p2 in P2 by XBOOLE_0:def 3;
A8:(TOP-REAL n)|P is_T2 by A6,TOPMETR:3;
P21 c= [#]((TOP-REAL n)|P) by A1,A4,XBOOLE_1:7;
then P2' is compact by A2,COMPTS_1:11;
then A9:P2' is closed by A8,COMPTS_1:16;
A10:P\P2= (P1 \P2) \/ (P2\P2) by A1,XBOOLE_1:42
.=(P1\P2) \/ {} by XBOOLE_1:37 .=P1\P2;
P1\P2=Q
proof
A11:P1\P2 c= Q
proof let x;assume x in P1\P2;
then A12:x in P1 & not x in P2 by XBOOLE_0:def 4;
then not x in {p1,p2} by A3,A7,TARSKI:def 2;
hence x in Q by A1,A12,XBOOLE_0:def 4;
end;
Q c= P1\P2
proof let x;assume x in Q;
then A13:x in P1 & not x in {p1,p2} by A1,XBOOLE_0:def 4;
then not x in P2 by A1,XBOOLE_0:def 3;
hence x in P1\P2 by A13,XBOOLE_0:def 4;
end;
hence thesis by A11,XBOOLE_0:def 10;
end;
then Q=P2'` by A5,A10,SUBSET_1:def 5;
then Q= P2'`;
hence thesis by A9,TOPS_1:29;
end;
theorem Th53:
for P being Subset of TOP-REAL n,
Q being Subset of (TOP-REAL n)|P,
p1,p2 being Point of TOP-REAL n st
P is_an_arc_of p1,p2 & Q=P\{p1,p2} holds Q is connected
proof let P be Subset of TOP-REAL n,
Q be Subset of (TOP-REAL n)|P,
p1,p2 be Point of TOP-REAL n;
assume A1:P is_an_arc_of p1,p2 & Q=P\{p1,p2};
then reconsider P' = P as non empty Subset of TOP-REAL n
by TOPREAL1:4;
consider f being map of I[01], (TOP-REAL n)|P' such that
A2: f is_homeomorphism & f.0 = p1 & f.1 = p2 by A1,TOPREAL1:def 2;
(the carrier of I[01]) \{0,1} is Subset of I[01]
by XBOOLE_1:36;
then reconsider P7=(the carrier of I[01]) \{0,1}
as Subset of I[01];
A3:P7<>{} & P7 is connected by Th48;
A4:f is continuous & f is one-to-one by A2,TOPS_2:def 5;
Q=f.:P7
proof
[#]((TOP-REAL n)|P)=P by PRE_TOPC:def 10;
then A5:rng f=P by A2,TOPS_2:def 5;
thus Q c= f.:P7
proof let x;assume x in Q;
then A6:x in P & not x in {p1,p2} by A1,XBOOLE_0:def 4;
then consider z being set such that
A7: z in dom f & x=f.z by A5,FUNCT_1:def 5;
A8: dom f=[#]I[01] by A2,TOPS_2:def 5;
now assume z in {0,1};
then x=p1 or x=p2 by A2,A7,TARSKI:def 2;
hence contradiction by A6,TARSKI:def 2;
end;
then z in P7 by A7,A8,XBOOLE_0:def 4;
hence x in f.:P7 by A7,FUNCT_1:def 12;
end;
let y;assume y in f.:P7;
then consider x such that
A9:x in dom f & x in P7 & y=f.x by FUNCT_1:def 12;
x in the carrier of I[01] & not x in {0,1} by A9,XBOOLE_0:def 4;
then A10:x<>0 & x<>1 by TARSKI:def 2;
A11:y in P by A5,A9,FUNCT_1:def 5;
now assume A12: y in {p1,p2};
reconsider f1=f as Function of the carrier of I[01],
the carrier of (TOP-REAL n)|P';
now per cases by A9,A12,TARSKI:def 2;
case A13:f.x=p1;
dom f1=the carrier of I[01] by FUNCT_2:def 1;
then 0 in dom f1 by BORSUK_1:83,TOPREAL5:1;
hence contradiction by A2,A4,A9,A10,A13,FUNCT_1:def 8;
case A14:f.x=p2;
dom f1=the carrier of I[01] by FUNCT_2:def 1;
then 1 in dom f1 by BORSUK_1:83,TOPREAL5:1;
hence contradiction by A2,A4,A9,A10,A14,FUNCT_1:def 8;
end;
hence contradiction;
end;
hence y in Q by A1,A11,XBOOLE_0:def 4;
end;
hence thesis by A3,A4,TOPREAL5:5;
end;
theorem Th54: for GX being non empty TopSpace,
P1, P being Subset of GX,
Q' being Subset of GX|P1,
Q being Subset of GX|P st P1 c=P & Q=Q' &
Q' is connected holds Q is connected
proof let GX be non empty TopSpace,
P1, P be Subset of GX,
Q' be Subset of GX|P1,
Q be Subset of GX|P;
assume A1: P1 c=P & Q=Q' & Q' is connected;
[#](GX|P)=P by PRE_TOPC:def 10;
then P1 is Subset of GX|P by A1,PRE_TOPC:12;
then reconsider P1'=P1 as Subset of GX|P;
GX|P1=(GX|P)|P1' by A1,Th47;
hence thesis by A1,CONNSP_3:34;
end;
theorem Th55:
for P being Subset of TOP-REAL n,
p1,p2 being Point of TOP-REAL n st
P is_an_arc_of p1,p2 ex p3 being Point of TOP-REAL n st
p3 in P & p3<>p1 & p3<>p2
proof let P be Subset of TOP-REAL n,
p1,p2 be Point of TOP-REAL n;
assume
P is_an_arc_of p1,p2;
then consider f being map of I[01], (TOP-REAL n)|P such that
A1:f is_homeomorphism & f.0 = p1 & f.1 = p2 by TOPREAL1:def 2;
1/2 in [.0,1.] by TOPREAL5:1;
then 1/2 in [#](I[01]) by BORSUK_1:83,PRE_TOPC:12;
then A2:1/2 in dom f by A1,TOPS_2:def 5;
then f.(1/2) in rng f by FUNCT_1:def 5;
then f.(1/2) in [#]((TOP-REAL n)|P) by A1,TOPS_2:def 5;
then A3:f.(1/2) in P by PRE_TOPC:def 10;
then reconsider p=f.(1/2) as Point of TOP-REAL n;
A4:f is one-to-one by A1,TOPS_2:def 5;
0 in the carrier of I[01] by BORSUK_1:83,TOPREAL5:1;
then 0 in [#](I[01]) by PRE_TOPC:12;
then 0 in dom f by A1,TOPS_2:def 5;
then A5:p1<>p by A1,A2,A4,FUNCT_1:def 8;
1 in [.0,1.] by TOPREAL5:1;
then 1 in [#](I[01]) by BORSUK_1:83,PRE_TOPC:12;
then 1 in dom f by A1,TOPS_2:def 5;
then f.1<>f.(1/2) by A2,A4,FUNCT_1:def 8;
hence thesis by A1,A3,A5;
end;
theorem
for P being Subset of TOP-REAL n,
p1,p2 being Point of TOP-REAL n st P is_an_arc_of p1,p2
holds P\{p1,p2}<>{}
proof let P be Subset of TOP-REAL n,
p1,p2 be Point of TOP-REAL n;
assume P is_an_arc_of p1,p2;
then consider p3 being Point of TOP-REAL n such that
A1: p3 in P & p3<>p1 & p3<>p2 by Th55;
not p3 in {p1,p2} by A1,TARSKI:def 2;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem
for P1 being Subset of TOP-REAL n,
P being Subset of TOP-REAL n,
Q being Subset of (TOP-REAL n)|P,
p1,p2 being Point of TOP-REAL n st
P1 is_an_arc_of p1,p2 & P1 c=P & Q=P1\{p1,p2} holds Q is connected
proof let P1 be Subset of TOP-REAL n,
P be Subset of TOP-REAL n,
Q be Subset of (TOP-REAL n)|P,
p1,p2 be Point of TOP-REAL n;
assume A1:P1 is_an_arc_of p1,p2 & P1 c=P & Q=P1\{p1,p2};
[#]((TOP-REAL n)|P1)=P1 by PRE_TOPC:def 10;
then the carrier of (TOP-REAL n)|P1=P1 by PRE_TOPC:12;
then Q is Subset of (TOP-REAL n)|P1 by A1,XBOOLE_1:36;
then reconsider Q'=Q as Subset of (TOP-REAL n)|P1;
Q' is connected by A1,Th53;
hence thesis by A1,Th54;
end;
theorem Th58: for T,S,V being non empty TopSpace,
P1 being non empty Subset of S,
P2 being Subset of S,
f being map of T,S|P1, g being map of S|P2,V st
P1 c= P2 & f is continuous & g is continuous
ex h being map of T,V st h=g*f & h is continuous
proof
let T,S,V be non empty TopSpace,
P1 be non empty Subset of S,
P2 be Subset of S,
f be map of T,S|P1, g be map of S|P2,V;
assume that A1: P1 c= P2 and
A2: f is continuous and A3: g is continuous;
reconsider P3 = P2 as non empty Subset of S by A1,XBOOLE_1:3;
reconsider g1 = g as map of S|P3,V;
[#](S|P1)=P1 by PRE_TOPC:def 10;
then the carrier of (S|P1)=P1 by PRE_TOPC:12;
then A4:f is Function of the carrier of T,P2 by A1,FUNCT_2:9;
A5: [#](S|P2)=P2 by PRE_TOPC:def 10;
then the carrier of (S|P2)=P2 by PRE_TOPC:12;
then reconsider f1=f as map of T,S|P3 by A4;
f1 is continuous
proof
for F1 being Subset of S|P2
st F1 is closed holds f1"F1 is closed
proof let F1 be Subset of S|P2;
assume A6:F1 is closed;
reconsider P1'=P1 as non empty Subset of S|P3 by A1,A5,
PRE_TOPC:12;
[#](S|P1)=P1 by PRE_TOPC:def 10;
then A7: the carrier of (S|P1)=P1 by PRE_TOPC:12;
reconsider P4=F1/\P1' as Subset of (S|P3)|P1'
by TOPS_2:38;
A8:S|P1=(S|P3)|P1' by A1,Th47;
A9: P4 is closed by A6,Th3;
A10:f1"P1=the carrier of T by A7,FUNCT_2:48
.=dom f1 by FUNCT_2:def 1;
f1"F1 c= dom f1 by RELAT_1:167;
then f1"F1=f1"F1 /\ f1"P1 by A10,XBOOLE_1:28
.=f"P4 by FUNCT_1:137;
hence f1"F1 is closed by A2,A8,A9,PRE_TOPC:def 12;
end;
hence f1 is continuous by PRE_TOPC:def 12;
end;
then g1*f1 is continuous by A3,TOPS_2:58;
hence thesis;
end;
theorem Th59:
for P1,P2 being Subset of TOP-REAL n,
p1,p2 being Point of TOP-REAL n st
P1 is_an_arc_of p1,p2 &
P2 is_an_arc_of p1,p2 & P1 c= P2 holds P1=P2
proof let P1,P2 be Subset of TOP-REAL n,
p1,p2 be Point of TOP-REAL n;
assume A1:P1 is_an_arc_of p1,p2 &
P2 is_an_arc_of p1,p2 & P1 c= P2;
then reconsider P1' = P1, P2' = P2
as non empty Subset of TOP-REAL n by TOPREAL1:4;
now assume A2:P2\P1<>{};consider p being Element of P2\P1;
A3:p in P2 & not p in P1 by A2,XBOOLE_0:def 4;
consider f1 being map of I[01],(TOP-REAL n)|P1' such that
A4:f1 is_homeomorphism & f1.0=p1 & f1.1=p2 by A1,TOPREAL1:def 2;
A5:f1 is continuous by A4,TOPS_2:def 5;
consider f2 being map of I[01],(TOP-REAL n)|P2' such that
A6:f2 is_homeomorphism & f2.0=p1 & f2.1=p2 by A1,TOPREAL1:def 2;
reconsider f4=f2 as Function;
A7:f2 is one-to-one by A6,TOPS_2:def 5;
A8:dom f2=[#](I[01]) & rng f2=[#]((TOP-REAL n)|P2) by A6,TOPS_2:def 5;
A9:f2" is_homeomorphism by A6,TOPS_2:70;
then A10:dom (f2")=[#]((TOP-REAL n)|P2) by TOPS_2:def 5
.=P2 by PRE_TOPC:def 10;
then A11:f2".p in rng (f2") by A3,FUNCT_1:def 5;
f2" is continuous by A6,TOPS_2:def 5;
then consider h being map of I[01],I[01] such that
A12:h=f2"*f1 & h is continuous by A1,A5,Th58;
h is Function of the carrier of Closed-Interval-TSpace(0,1),
the carrier of R^1 by BORSUK_1:83,FUNCT_2:9,TOPMETR:24,27;
then reconsider h1=h as map of Closed-Interval-TSpace(0,1),R^1
;
h1 is continuous
proof
for F1 being Subset of R^1 st F1 is closed holds h1"F1 is closed
proof let F1 be Subset of R^1;
assume A13:F1 is closed;
reconsider K=the carrier of I[01]
as Subset of R^1 by BORSUK_1:83,TOPMETR:24;
A14:I[01]=R^1|K by BORSUK_1:83,TOPMETR:26,27;
reconsider P3=F1/\K as Subset of R^1|K by TOPS_2:38;
A15: P3 is closed by A13,Th3;
A16:h1"K=the carrier of I[01] by FUNCT_2:48
.=dom h1 by FUNCT_2:def 1;
h1"F1 c= dom h1 by RELAT_1:167;
then h1"F1=h1"F1 /\ h1"K by A16,XBOOLE_1:28
.=h"P3 by FUNCT_1:137;
hence h1"F1 is closed by A12,A14,A15,PRE_TOPC:def 12,TOPMETR:27;
end;
hence h1 is continuous by PRE_TOPC:def 12;
end;
then reconsider g=h1 as continuous map of
Closed-Interval-TSpace(0,1),R^1;
A17:dom f1 =[#](I[01]) by A4,TOPS_2:def 5
.=[.0,1.] by BORSUK_1:83,PRE_TOPC:12;
then A18:0 in dom f1 by TOPREAL5:1;
A19:1 in dom f1 by A17,TOPREAL5:1;
A20:g.0=f2".p1 by A4,A12,A18,FUNCT_1:23;
A21:g.1=f2".p2 by A4,A12,A19,FUNCT_1:23;
A22:dom f2 =[#](I[01]) by A6,TOPS_2:def 5
.=[.0,1.] by BORSUK_1:83,PRE_TOPC:12;
then A23:0 in dom f2 by TOPREAL5:1;
A24:1 in dom f2 by A22,TOPREAL5:1;
A25:(f2").p1=(f4").p1 by A7,A8,TOPS_2:def 4;
((f2)").p2=(f4").p2 by A7,A8,TOPS_2:def 4;
then A26:g.0=0 & g.1=1 by A6,A7,A20,A21,A23,A24,A25,FUNCT_1:54;
A27:f2".p in [.0,1.] by A11,BORSUK_1:83;
A28:now assume f2".p in rng g;
then consider x being set such that
A29:x in dom g & f2".p=g.x by FUNCT_1:def 5;
A30:f2".p=f2".(f1.x) by A12,A29,FUNCT_1:22;
A31:x in dom f1 & f1.x in dom (f2") by A12,A29,FUNCT_1:21;
f2" is one-to-one by A9,TOPS_2:def 5;
then p=f1.x by A3,A10,A30,A31,FUNCT_1:def 8;
then A32:p in rng f1 by A31,FUNCT_1:def 5;
rng f1 =[#]((TOP-REAL n)|P1) by A4,TOPS_2:def 5
.=P1 by PRE_TOPC:def 10;
hence contradiction by A2,A32,XBOOLE_0:def 4;
end;
reconsider r=f2".p as Real by A27;
A33:rng f2=[#]((TOP-REAL n)|P2) by A6,TOPS_2:def 5 .=P2
by PRE_TOPC:def 10;
A34:0<=r & r<=1 by A11,BORSUK_1:83,TOPREAL5:1;
A35: now assume A36:r=0;
f2.r=f4.((f4").p) by A7,A8,TOPS_2:def 4
.=p by A3,A7,A33,FUNCT_1:57;
hence contradiction by A1,A3,A6,A36,TOPREAL1:4;
end;
now assume A37:r=1;
f2.r= f4.((f4").p) by A7,A8,TOPS_2:def 4
.=p by A3,A7,A33,FUNCT_1:57;
hence contradiction by A1,A3,A6,A37,TOPREAL1:4;
end;
then 0<r & r<1 by A34,A35,REAL_1:def 5;
then consider rc being Real such that
A38:g.rc=r & 0<rc & rc <1 by A26,TOPREAL5:12;
the carrier of (TOP-REAL n)|P1 =
[#]((TOP-REAL n)|P1) by PRE_TOPC:12 .=P1 by PRE_TOPC:def 10;
then rng f1 c= dom (f2") by A1,A10,XBOOLE_1:1;
then dom g=dom f1 by A12,RELAT_1:46 .=[#](I[01]) by A4,TOPS_2:def 5
.=[.0,1.] by BORSUK_1:83,PRE_TOPC:12;
then rc in dom g by A38,TOPREAL5:1;
hence contradiction by A28,A38,FUNCT_1:def 5;
end;
then P2 c= P1 by XBOOLE_1:37;
hence P1=P2 by A1,XBOOLE_0:def 10;
end;
theorem Th60:for P being non empty Subset of TOP-REAL 2,
Q being Subset of (TOP-REAL 2)|P,
p1,p2 being Point of TOP-REAL 2
st P is_simple_closed_curve & p1 in P & p2 in P & p1<>p2 & Q=P\{p1,p2}
holds not Q is connected
proof let P be non empty Subset of TOP-REAL 2,
Q be Subset of (TOP-REAL 2)|P,
p1,p2 be Point of TOP-REAL 2;
assume
A1:P is_simple_closed_curve & p1 in P & p2 in P & p1<>p2 & Q=P\{p1,p2};
then consider P1,P2 being non empty Subset of TOP-REAL 2
such that
A2: P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 &
P = P1 \/ P2 & P1 /\ P2 = {p1,p2} by TOPREAL2:5;
[#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 10;
then A3:the carrier of (TOP-REAL 2)|P=P by PRE_TOPC:12;
A4:P1 c= P by A2,XBOOLE_1:7;
P1\{p1,p2} c= P1 by XBOOLE_1:36;
then P1\{p1,p2} is Subset of (TOP-REAL 2)|P by A3,A4,XBOOLE_1
:1;
then reconsider P1'=P1\{p1,p2} as Subset of (TOP-REAL 2)|P;
A5:P2 c= P by A2,XBOOLE_1:7;
P2\{p1,p2} c= P2 by XBOOLE_1:36;
then P2\{p1,p2} is Subset of (TOP-REAL 2)|P by A3,A5,XBOOLE_1
:1;
then reconsider P2'=P2\{p1,p2} as Subset of (TOP-REAL 2)|P;
A6:P1' is open by A1,A2,Th52;
A7:P2' is open by A1,A2,Th52;
A8:Q c= P1' \/ P2'
proof let x;assume x in Q;
then A9: x in P & not x in {p1,p2} by A1,XBOOLE_0:def 4;
now per cases by A2,A9,XBOOLE_0:def 2;
case (x in P1 & not x in {p1,p2});
then x in P1' by XBOOLE_0:def 4;
hence x in P1' \/ P2' by XBOOLE_0:def 2;
case (x in P2 & not x in {p1,p2});
then x in P2' by XBOOLE_0:def 4;
hence x in P1' \/ P2' by XBOOLE_0:def 2;
end;
hence x in P1' \/ P2';
end;
consider p3 being Point of TOP-REAL 2 such that
A10:p3 in P1 & p3<>p1 & p3<>p2 by A2,Th55;
not p3 in {p1,p2} by A10,TARSKI:def 2;
then A11:P1'<>{} by A10,XBOOLE_0:def 4;
P1' c= Q
proof let x;assume x in P1';
then A12:x in P1 & not x in {p1,p2} by XBOOLE_0:def 4;
then x in P by A2,XBOOLE_0:def 2;
hence x in Q by A1,A12,XBOOLE_0:def 4;
end;
then (P1' /\ Q) <>{} by A11,XBOOLE_1:28;
then A13:P1' meets Q by XBOOLE_0:def 7;
consider p3' being Point of TOP-REAL 2 such that
A14:p3' in P2 & p3'<>p1 & p3'<>p2 by A2,Th55;
not p3' in {p1,p2} by A14,TARSKI:def 2;
then A15:P2'<>{} by A14,XBOOLE_0:def 4;
P2' c= Q
proof let x;assume x in P2';
then A16:x in P2 & not x in {p1,p2} by XBOOLE_0:def 4;
then x in P1 \/ P2 by XBOOLE_0:def 2;
hence x in Q by A1,A2,A16,XBOOLE_0:def 4;
end;
then P2' /\ Q<>{} by A15,XBOOLE_1:28;
then A17:P2' meets Q by XBOOLE_0:def 7;
now assume P1' meets P2';
then consider p0 being set such that
A18:p0 in P1' & p0 in P2' by XBOOLE_0:3;
A19:p0 in P1 & not p0 in {p1,p2} by A18,XBOOLE_0:def 4;
p0 in P2 by A18,XBOOLE_0:def 4;
hence contradiction by A2,A19,XBOOLE_0:def 3;
end;
hence thesis by A6,A7,A8,A13,A17,TOPREAL5:4;
end;
theorem Th61:
for P being non empty Subset of TOP-REAL 2,
P1,P2,P1',P2' being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2
st P is_simple_closed_curve
& P1 is_an_arc_of p1,p2
& P2 is_an_arc_of p1,p2 & P1 \/ P2=P
& P1' is_an_arc_of p1,p2
& P2' is_an_arc_of p1,p2 & P1' \/ P2'=P
holds P1=P1' & P2=P2' or P1=P2' & P2=P1'
proof let P be non empty Subset of TOP-REAL 2,
P1,P2,P1',P2' be Subset of
the carrier of TOP-REAL 2,p1,p2 be Point of TOP-REAL 2;
assume that
A1: P is_simple_closed_curve and
A2: P1 is_an_arc_of p1,p2 and
A3: P2 is_an_arc_of p1,p2 and
A4: P1 \/ P2=P and
A5: P1' is_an_arc_of p1,p2 and
A6: P2' is_an_arc_of p1,p2 and
A7: P1' \/ P2'=P;
A8:p1<>p2 by A6,Th49;
A9:P2' c= P by A7,XBOOLE_1:7;
A10:p1 in P1' & p2 in P1' by A5,TOPREAL1:4;
A11:P1' c= P by A7,XBOOLE_1:7;
A12:p1 in P2 & p2 in P2 by A3,TOPREAL1:4;
A13:p1 in P1 & p2 in P1 by A2,TOPREAL1:4;
A14:P1 c= P by A4,XBOOLE_1:7;
[#]((TOP-REAL 2)|P)=P by PRE_TOPC:def 10;
then A15:the carrier of (TOP-REAL 2)|P=P by PRE_TOPC:12;
P1\{p1,p2} c= P1 by XBOOLE_1:36;
then P1\{p1,p2} is Subset of (TOP-REAL 2)|P
by A14,A15,XBOOLE_1:1;
then reconsider Q1=P1\{p1,p2} as Subset of (TOP-REAL 2)|P;
A16:Q1 c= P1 by XBOOLE_1:36;
A17:P2 c= P by A4,XBOOLE_1:7;
P2\{p1,p2} c= P2 by XBOOLE_1:36;
then P2\{p1,p2} is Subset of (TOP-REAL 2)|P
by A15,A17,XBOOLE_1:1;
then reconsider Q2=P2\{p1,p2} as Subset of (TOP-REAL 2)|P;
A18:Q2 c= P2 by XBOOLE_1:36;
A19:P1' c= P by A7,XBOOLE_1:7;
P1'\{p1,p2} c= P1' by XBOOLE_1:36;
then P1'\{p1,p2} is Subset of (TOP-REAL 2)|P
by A15,A19,XBOOLE_1:1;
then reconsider Q1'=P1'\{p1,p2} as Subset of (TOP-REAL 2)|P;
A20:Q1' c= P1' by XBOOLE_1:36;
A21:P2' c= P by A7,XBOOLE_1:7;
P2'\{p1,p2} c= P2' by XBOOLE_1:36;
then P2'\{p1,p2} is Subset of (TOP-REAL 2)|P
by A15,A21,XBOOLE_1:1;
then reconsider Q2'=P2'\{p1,p2} as Subset of (TOP-REAL 2)|P;
A22:Q2' c= P2' by XBOOLE_1:36;
A23:Q1 \/ Q2 =P\{p1,p2} by A4,XBOOLE_1:42;
A24:Q1' \/ Q2' =P\{p1,p2} by A7,XBOOLE_1:42;
then Q1' c=Q1 \/ Q2 by A23,XBOOLE_1:7;
then A25:Q1' \/ (Q1 \/ Q2)=Q1 \/ Q2 by XBOOLE_1:12;
Q2' c=Q1 \/ Q2 by A23,A24,XBOOLE_1:7;
then A26:Q2' \/ (Q1 \/ Q2)=Q1 \/ Q2 by XBOOLE_1:12;
Q1 c=Q1' \/ Q2' by A23,A24,XBOOLE_1:7;
then A27:Q1 \/ (Q1' \/ Q2')=Q1' \/ Q2' by XBOOLE_1:12;
Q2 c=Q1' \/ Q2' by A23,A24,XBOOLE_1:7;
then A28:Q2 \/ (Q1' \/ Q2')=Q1' \/ Q2' by XBOOLE_1:12;
[#]((TOP-REAL 2)|P1)=P1 by PRE_TOPC:def 10;
then Q1 is Subset of (TOP-REAL 2)|P1 by A16,PRE_TOPC:12;
then reconsider R1=Q1 as Subset of (TOP-REAL 2)|P1;
R1 is connected by A2,Th53;
then A29:Q1 is connected by A14,Th54;
[#]((TOP-REAL 2)|P2)=P2 by PRE_TOPC:def 10;
then Q2 is Subset of (TOP-REAL 2)|P2 by A18,PRE_TOPC:12;
then reconsider R2=Q2 as Subset of (TOP-REAL 2)|P2;
R2 is connected by A3,Th53;
then A30:Q2 is connected by A17,Th54;
[#]((TOP-REAL 2)|P1')=P1' by PRE_TOPC:def 10;
then Q1' is Subset of (TOP-REAL 2)|P1' by A20,PRE_TOPC:12;
then reconsider R1'=Q1' as Subset of (TOP-REAL 2)|P1';
R1' is connected by A5,Th53;
then A31:Q1' is connected by A11,Th54;
[#]((TOP-REAL 2)|P2')=P2' by PRE_TOPC:def 10;
then Q2' is Subset of (TOP-REAL 2)|P2' by A22,PRE_TOPC:12;
then reconsider R2'=Q2' as Subset of (TOP-REAL 2)|P2';
R2' is connected by A6,Th53;
then A32:Q2' is connected by A9,Th54;
A33: {p1,p2} c= P1
proof let x;assume x in {p1,p2};
hence x in P1 by A13,TARSKI:def 2;
end;
A34: {p1,p2} c= P2
proof let x;assume x in {p1,p2};
hence x in P2 by A12,TARSKI:def 2;
end;
A35: {p1,p2} c= P1'
proof let x;assume x in {p1,p2};
hence x in P1' by A10,TARSKI:def 2;
end;
A36: {p1,p2} c= P2'
proof let x;assume x in {p1,p2};
then x=p1 or x=p2 by TARSKI:def 2;
hence x in P2' by A6,TOPREAL1:4;
end;
A37:Q1 \/ {p1,p2}=P1 by A33,XBOOLE_1:45;
A38:Q2 \/ {p1,p2}=P2 by A34,XBOOLE_1:45;
A39:Q1' \/ {p1,p2}=P1' by A35,XBOOLE_1:45;
A40:Q2' \/ {p1,p2}=P2' by A36,XBOOLE_1:45;
now assume
A41: not(P1=P2' & P2=P1');
now per cases by A41;
case A42:P1<>P2';
A43: now assume A44:Q1\Q2'={} & Q2'\Q1={};
then A45:Q1 c= Q2' by XBOOLE_1:37;
Q2' c= Q1 by A44,XBOOLE_1:37;
hence contradiction by A37,A40,A42,A45,XBOOLE_0:def 10;
end;
now per cases by A43;
case A46:Q1\Q2'<>{};
consider y being Element of Q1\Q2';
A47:y in Q1 by A46,XBOOLE_0:def 4;
then A48:y in Q1' \/ Q2' by A23,A24,XBOOLE_0:def 2;
not y in Q2' by A46,XBOOLE_0:def 4;
then y in Q1' by A48,XBOOLE_0:def 2;
then Q1 /\ Q1'<>{} by A47,XBOOLE_0:def 3;
then A49:Q1 meets Q1' by XBOOLE_0:def 7;
now assume Q2 meets Q1';
then A50:Q1 \/ Q1' \/ Q2 is connected by A29,A30,A31,A49,JORDAN1:7;
Q1 \/ Q1' \/ Q2=P\{p1,p2} by A23,A25,XBOOLE_1:4;
hence contradiction by A1,A8,A13,A14,A50,Th60;
end;
then A51: Q2/\Q1'={} by XBOOLE_0:def 7;
Q2 c= Q2'
proof let x;assume
A52:x in Q2; then x in Q1 \/ Q2 by XBOOLE_0:def 2;
then x in Q1' or x in Q2' by A23,A24,XBOOLE_0:def 2;
hence x in Q2' by A51,A52,XBOOLE_0:def 3;
end;
then A53: P2 c= P2' by A38,A40,XBOOLE_1:9;
Q1' c= Q1
proof let x;assume
A54:x in Q1';
then x in Q1 \/ Q2 by A23,A24,XBOOLE_0:def 2;
then x in Q1 or x in Q2 by XBOOLE_0:def 2;
hence x in Q1 by A51,A54,XBOOLE_0:def 3;
end;
then P1' c= P1 by A37,A39,XBOOLE_1:9;
hence P1=P1' & P2=P2' or P1=P2' & P2=P1'
by A2,A3,A5,A6,A53,Th59;
case A55:Q2'\Q1<>{};
consider y being Element of Q2'\Q1;
A56:y in Q2' by A55,XBOOLE_0:def 4;
then A57:y in Q2 \/ Q1 by A23,A24,XBOOLE_0:def 2;
not y in Q1 by A55,XBOOLE_0:def 4;
then y in Q2 by A57,XBOOLE_0:def 2;
then Q2' /\ Q2<>{} by A56,XBOOLE_0:def 3;
then A58:Q2' meets Q2 by XBOOLE_0:def 7;
now assume Q1' meets Q2;
then A59:Q2' \/ Q2 \/ Q1' is connected by A30,A31,A32,A58,JORDAN1:7;
Q2' \/ Q2 \/ Q1'=P\{p1,p2} by A24,A28,XBOOLE_1:4;
hence contradiction by A1,A8,A13,A14,A59,Th60;
end;
then A60: Q1'/\Q2={} by XBOOLE_0:def 7;
Q1' c= Q1
proof let x;assume
A61:x in Q1'; then x in Q1' \/ Q2' by XBOOLE_0:def 2;
then x in Q1 or x in Q2 by A23,A24,XBOOLE_0:def 2;
hence x in Q1 by A60,A61,XBOOLE_0:def 3;
end;
then A62: P1' c= P1 by A37,A39,XBOOLE_1:9;
Q2 c= Q2'
proof let x;assume
A63:x in Q2; then x in Q2 \/ Q1 by XBOOLE_0:def 2;
then x in Q2' or x in Q1' by A23,A24,XBOOLE_0:def 2;
hence x in Q2' by A60,A63,XBOOLE_0:def 3;
end;
then P2 c= P2' by A38,A40,XBOOLE_1:9;
hence P1=P1' & P2=P2' or P1=P2' & P2=P1'
by A2,A3,A5,A6,A62,Th59;
end;
hence P1=P1' & P2=P2' or P1=P2' & P2=P1';
case A64: P2<>P1';
A65: now assume A66:Q2\Q1'={} & Q1'\Q2={};
then A67:Q2 c= Q1' by XBOOLE_1:37;
Q1' c= Q2 by A66,XBOOLE_1:37;
hence contradiction by A38,A39,A64,A67,XBOOLE_0:def 10;
end;
now per cases by A65;
case A68:Q2\Q1'<>{};
consider y being Element of Q2\Q1';
A69:y in Q2 by A68,XBOOLE_0:def 4;
then A70:y in Q2' \/ Q1' by A23,A24,XBOOLE_0:def 2;
not y in Q1' by A68,XBOOLE_0:def 4;
then y in Q2' by A70,XBOOLE_0:def 2;
then Q2 /\ Q2'<>{} by A69,XBOOLE_0:def 3;
then A71:Q2 meets Q2' by XBOOLE_0:def 7;
now assume Q1 meets Q2';
then A72:Q2 \/ Q2' \/ Q1 is connected by A29,A30,A32,A71,JORDAN1:7;
Q2 \/ Q2' \/ Q1=P\{p1,p2} by A23,A26,XBOOLE_1:4;
hence contradiction by A1,A8,A13,A14,A72,Th60;
end;
then A73: Q1/\Q2'={} by XBOOLE_0:def 7;
Q1 c= Q1'
proof let x;assume
A74:x in Q1; then x in Q2 \/ Q1 by XBOOLE_0:def 2;
then x in Q2' or x in Q1' by A23,A24,XBOOLE_0:def 2;
hence x in Q1' by A73,A74,XBOOLE_0:def 3;
end;
then A75: P1 c= P1' by A37,A39,XBOOLE_1:9;
Q2' c= Q2
proof let x;assume
A76:x in Q2';
then x in Q2 \/ Q1 by A23,A24,XBOOLE_0:def 2;
then x in Q2 or x in Q1 by XBOOLE_0:def 2;
hence x in Q2 by A73,A76,XBOOLE_0:def 3;
end;
then P2' c= P2 by A38,A40,XBOOLE_1:9;
hence P1=P1' & P2=P2' or P1=P2' & P2=P1'
by A2,A3,A5,A6,A75,Th59;
case A77:Q1'\Q2<>{};
consider y being Element of Q1'\Q2;
A78:y in Q1' by A77,XBOOLE_0:def 4;
then A79:y in Q1 \/ Q2 by A23,A24,XBOOLE_0:def 2;
not y in Q2 by A77,XBOOLE_0:def 4;
then y in Q1 by A79,XBOOLE_0:def 2;
then Q1' /\ Q1<>{} by A78,XBOOLE_0:def 3;
then A80:Q1' meets Q1 by XBOOLE_0:def 7;
now assume Q2' meets Q1;
then A81:Q1' \/ Q1 \/ Q2' is connected by A29,A31,A32,A80,JORDAN1:7;
Q1' \/ Q1 \/ Q2'=P\{p1,p2} by A24,A27,XBOOLE_1:4;
hence contradiction by A1,A8,A13,A14,A81,Th60;
end;
then A82: Q2' /\ Q1 = {} by XBOOLE_0:def 7;
Q2' c= Q2
proof let x;assume
A83:x in Q2'; then x in Q2' \/ Q1' by XBOOLE_0:def 2;
then x in Q2 or x in Q1 by A23,A24,XBOOLE_0:def 2;
hence x in Q2 by A82,A83,XBOOLE_0:def 3;
end;
then A84: P2' c= P2 by A38,A40,XBOOLE_1:9;
Q1 c= Q1'
proof let x;assume
A85:x in Q1;
then x in Q1' \/ Q2' by A23,A24,XBOOLE_0:def 2;
then x in Q1' or x in Q2' by XBOOLE_0:def 2;
hence x in Q1' by A82,A85,XBOOLE_0:def 3;
end;
then P1 c= P1' by A37,A39,XBOOLE_1:9;
hence P1=P1' & P2=P2' or P1=P2' & P2=P1'
by A2,A3,A5,A6,A84,Th59;
end;
hence P1=P1' & P2=P2' or P1=P2' & P2=P1';
end;
hence P1=P1' & P2=P2' or P1=P2' & P2=P1';
end;
hence thesis;
end;
begin ::Lower Arcs and Upper Arcs
definition
cluster -> real Element of R^1;
coherence by TOPMETR:24,XREAL_0:def 1;
end;
Lm1: for g being map of I[01],R^1,
s1,s2,r being Real st g is continuous &
g.0[01] < r & r < g.1[01] & s1=g.0 & s2=g.1 ex r1 st 0<r1 & r1<1 & g.r1=r
proof let g be map of I[01],R^1,s1,s2,r be Real;
assume g is continuous &
g.0[01] < r & r < g.1[01] & s1=g.0 & s2=g.1;
then ex rc being Real st
g.rc=r & 0<rc & rc <1 by BORSUK_1:def 17,def 18,TOPMETR:27,TOPREAL5:12;
hence thesis;
end;
canceled 2;
theorem Th64:
for P1 being Subset of TOP-REAL 2,
r being Real,p1,p2 being Point of TOP-REAL 2 st
p1`1<=r & r<=p2`1 & P1 is_an_arc_of p1,p2
holds P1 meets Vertical_Line(r) &
P1 /\ Vertical_Line(r) is closed
proof let P1 be Subset of TOP-REAL 2,
r be Real,
p1,p2 be Point of TOP-REAL 2;
assume A1: p1`1<=r & r<=p2`1 & P1 is_an_arc_of p1,p2;
then reconsider P1' = P1
as non empty Subset of TOP-REAL 2 by TOPREAL1:4;
consider f being map of I[01], (TOP-REAL 2)|P1' such that
A2: f is_homeomorphism & f.0 = p1 & f.1 = p2 by A1,TOPREAL1:def 2;
[#]((TOP-REAL 2)|P1)=P1 by PRE_TOPC:def 10;
then A3:the carrier of (TOP-REAL 2)|P1=P1 by PRE_TOPC:12;
then reconsider f1=f as Function of the carrier of I[01],
the carrier of TOP-REAL 2 by FUNCT_2:9;
reconsider f2=f1 as map of I[01],TOP-REAL 2 ;
reconsider proj11=proj1 as Function of the carrier of TOP-REAL 2,REAL;
reconsider proj12=proj1 as map of TOP-REAL 2,R^1 by TOPMETR:24;
reconsider g1=proj11*f1 as Function of the carrier of I[01],REAL;
reconsider g=g1 as map of I[01],R^1 by TOPMETR:24;
f is continuous by A2,TOPS_2:def 5;
then A4:f2 is continuous by Th4;
proj12 is continuous by TOPREAL5:16;
then A5:g is continuous by A4,TOPS_2:58;
A6:dom f=[.0,1.] by BORSUK_1:83,FUNCT_2:def 1;
then A7:0 in dom f by TOPREAL5:1;
A8:1 in dom f by A6,TOPREAL5:1;
A9:g.0=proj1.p1 by A2,A7,FUNCT_1:23 .=p1`1
by PSCOMP_1:def 28;
A10: g.1=proj1.p2 by A2,A8,FUNCT_1:23 .=p2`1
by PSCOMP_1:def 28;
reconsider P1' as non empty Subset of TOP-REAL 2;
A11:P1' is closed by A1,Th12;
A12: Vertical_Line(r) is closed by Th33;
now per cases by A1,A9,A10,AXIOMS:21,BORSUK_1:def 17,def 18;
case g.0=g.1;
then A13:g.0=r by A1,A9,A10,AXIOMS:21;
A14:0 in dom f by A6,TOPREAL5:1;
then A15: f.0 in rng f by FUNCT_1:def 5;
then f.0 in P1 by A3;
then reconsider p=f.0 as Point of TOP-REAL 2;
p`1=proj1.(f.0) by PSCOMP_1:def 28
.=r by A13,A14,FUNCT_1:23;
then f.0 in {q where q is Point of TOP-REAL 2: q`1=r};
then f.0 in Vertical_Line(r) by Def6;
hence P1 meets Vertical_Line(r) by A3,A15,XBOOLE_0:3;
case A16: g.0[01]=r;
A17:0 in dom f by A6,TOPREAL5:1;
then A18: f.0 in rng f by FUNCT_1:def 5;
then f.0 in P1 by A3;
then reconsider p=f.0 as Point of TOP-REAL 2;
p`1=proj1.(f.0) by PSCOMP_1:def 28
.=r by A16,A17,BORSUK_1:def 17,FUNCT_1:23;
then f.0 in {q where q is Point of TOP-REAL 2: q`1=r};
then f.0 in Vertical_Line(r) by Def6;
hence P1 meets Vertical_Line(r) by A3,A18,XBOOLE_0:3;
case A19: g.1[01]=r;
A20:1 in dom f by A6,TOPREAL5:1;
then A21: f.1 in rng f by FUNCT_1:def 5;
then f.1 in P1 by A3;
then reconsider p=f.1 as Point of TOP-REAL 2;
p`1=proj1.(f.1) by PSCOMP_1:def 28
.=r by A19,A20,BORSUK_1:def 18,FUNCT_1:23;
then f.1 in {q where q is Point of TOP-REAL 2: q`1=r};
then f.1 in Vertical_Line(r) by Def6;
hence P1 meets Vertical_Line(r) by A3,A21,XBOOLE_0:3;
case g.0[01]< r & r < g.1[01];
then consider r1 such that A22:0<r1 & r1<1 & g.r1=r by A5,A9,A10,Lm1;
dom f=[.0,1.] by BORSUK_1:83,FUNCT_2:def 1;
then A23:r1 in dom f by A22,TOPREAL5:1;
[#]((TOP-REAL 2)|P1)=P1 by PRE_TOPC:def 10;
then A24:the carrier of (TOP-REAL 2)|P1=P1 by PRE_TOPC:12;
A25: f.r1 in rng f by A23,FUNCT_1:def 5;
then f.r1 in P1 by A24;
then reconsider p=f.r1 as Point of TOP-REAL 2;
p`1=proj1.(f.r1) by PSCOMP_1:def 28
.=r by A22,A23,FUNCT_1:23;
then f.r1 in {q where q is Point of TOP-REAL 2: q`1=r};
then f.r1 in Vertical_Line(r) by Def6;
hence P1 meets Vertical_Line(r) by A24,A25,XBOOLE_0:3;
end;
hence thesis by A11,A12,TOPS_1:35;
end;
Lm2:now let P be compact non empty Subset of TOP-REAL 2;
assume A1:P is_simple_closed_curve;
let P1,P1' be non empty Subset of TOP-REAL 2;
assume A2:( ex P2 being non empty Subset of TOP-REAL 2 st
P1 is_an_arc_of W-min(P),E-max(P)
& P2 is_an_arc_of E-max(P),W-min(P)
& P1 /\ P2={W-min(P),E-max(P)}
& P1 \/ P2=P
& First_Point(P1,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(P2,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2) &
( ex P2' being non empty Subset of TOP-REAL 2 st
P1' is_an_arc_of W-min(P),E-max(P)
& P2' is_an_arc_of E-max(P),W-min(P)
& P1' /\ P2'={W-min(P),E-max(P)}
& P1' \/ P2'=P
& First_Point(P1',W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(P2',E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2);
then consider
P2 being non empty Subset of TOP-REAL 2 such that
A3:P1 is_an_arc_of W-min(P),E-max(P)
& P2 is_an_arc_of E-max(P),W-min(P)
& P1 /\ P2={W-min(P),E-max(P)}
& P1 \/ P2=P
& First_Point(P1,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(P2,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2;
A4:P2 is_an_arc_of W-min(P),E-max(P) by A3,JORDAN5B:14;
consider
P2' being non empty Subset of TOP-REAL 2 such that
A5:P1' is_an_arc_of W-min(P),E-max(P)
& P2' is_an_arc_of E-max(P),W-min(P)
& P1' /\ P2'={W-min(P),E-max(P)}
& P1' \/ P2'=P
& First_Point(P1',W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(P2',E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2 by A2;
A6:P2' is_an_arc_of W-min(P),E-max(P) by A5,JORDAN5B:14;
now assume A7:P1=P2' & P2=P1';
A8:(W-min(P))`1=W-bound(P) by PSCOMP_1:84;
A9:(E-max(P))`1=E-bound(P) by PSCOMP_1:104;
then (W-min(P))`1<(E-max(P))`1 by A1,A8,TOPREAL5:23;
then A10: (W-min P)`1<=(W-bound(P)+E-bound(P))/2 &
(W-bound(P)+E-bound(P))/2<=(E-max P)`1 by A8,A9,TOPREAL3:3;
then P2 meets Vertical_Line((W-bound(P)+E-bound(P))/2) &
P2 /\ Vertical_Line((W-bound(P)+E-bound(P))/2) is closed
by A4,Th64;
then A11:First_Point(P1,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
First_Point(P2,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2
by A3,JORDAN5C:18;
P2' meets Vertical_Line((W-bound(P)+E-bound(P))/2) &
P2' /\ Vertical_Line((W-bound(P)+E-bound(P))/2) is closed
by A6,A10,Th64;
hence contradiction by A5,A7,A11,JORDAN5C:18;
end;
hence P1=P1' by A1,A3,A4,A5,A6,Th61;
end;
definition let P be compact non empty Subset of TOP-REAL 2
such that A1:P is_simple_closed_curve;
func Upper_Arc(P) -> non empty Subset of TOP-REAL 2 means
:Def8:
it is_an_arc_of W-min(P),E-max(P) &
ex P2 being non empty Subset of TOP-REAL 2 st
P2 is_an_arc_of E-max(P),W-min(P)
& it /\ P2={W-min(P),E-max(P)}
& it \/ P2=P
& First_Point(it,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(P2,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2;
existence
proof
ex P1,P2 being non empty Subset of TOP-REAL 2 st
P1 is_an_arc_of W-min(P),E-max(P)
& P2 is_an_arc_of E-max(P),W-min(P)
& P1 /\ P2={W-min(P),E-max(P)}
& P1 \/ P2=P
& First_Point(P1,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(P2,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2 by A1,Th40;
hence thesis;
end;
uniqueness by A1,Lm2;
end;
definition let P be compact non empty Subset of TOP-REAL 2; assume
A1:P is_simple_closed_curve;
then A2:Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by Def8;
func Lower_Arc(P) -> non empty Subset of TOP-REAL 2 means
:Def9:
it is_an_arc_of E-max(P),W-min(P)
& Upper_Arc(P) /\ it={W-min(P),E-max(P)}
& Upper_Arc(P) \/ it=P
& First_Point(Upper_Arc(P),W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(it,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2;
existence by A1,Def8;
uniqueness
proof
let P1,P1' be non empty Subset of TOP-REAL 2;
assume A3:( P1 is_an_arc_of E-max(P),W-min(P)
& Upper_Arc(P) /\ P1={W-min(P),E-max(P)}
& Upper_Arc(P) \/ P1=P
& First_Point(Upper_Arc(P),W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(P1,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2) &
( P1' is_an_arc_of E-max(P),W-min(P)
& Upper_Arc(P) /\ P1'={W-min(P),E-max(P)}
& Upper_Arc(P) \/ P1'=P
& First_Point(Upper_Arc(P),W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(P1',E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2);
then A4:P1 is_an_arc_of W-min(P),E-max(P) by JORDAN5B:14;
P1' is_an_arc_of W-min(P),E-max(P) by A3,JORDAN5B:14;
then P1=P1' or
Upper_Arc(P)=P1' & P1=Upper_Arc(P) by A1,A2,A3,A4,Th61;
hence P1=P1';
end;
end;
theorem Th65:for P being compact non empty Subset of (TOP-REAL 2)
st P is_simple_closed_curve holds
Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) &
Upper_Arc(P) is_an_arc_of E-max(P),W-min(P) &
Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) &
Lower_Arc(P) is_an_arc_of W-min(P),E-max(P) &
Upper_Arc(P) /\ Lower_Arc(P)={W-min(P),E-max(P)}
& Upper_Arc(P) \/ Lower_Arc(P)=P
& First_Point(Upper_Arc(P),W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(Lower_Arc(P),E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2
proof let P be compact non empty Subset of (TOP-REAL 2);
assume A1:P is_simple_closed_curve;
then A2: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by Def8;
Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by A1,Def9;
hence thesis by A1,A2,Def9,JORDAN5B:14;
end;
theorem Th66: for P being compact non empty Subset of (TOP-REAL 2)
st P is_simple_closed_curve
holds Lower_Arc(P)=(P\Upper_Arc(P)) \/ {W-min(P),E-max(P)} &
Upper_Arc(P)=(P\Lower_Arc(P)) \/ {W-min(P),E-max(P)}
proof let P be compact non empty Subset of (TOP-REAL 2);
assume P is_simple_closed_curve;
then A1: Upper_Arc(P) /\ Lower_Arc(P)={W-min(P),E-max(P)}
& Upper_Arc(P) \/ Lower_Arc(P)=P by Def9;
set B=Upper_Arc(P),A=Lower_Arc(P);
A2: (B \/ A \B)\/ (B /\ A) =(A \ B) \/ (A/\B) by XBOOLE_1:40 .=A by XBOOLE_1:
51
;
(B \/ A \A)\/ (B /\ A)
=(B \ A) \/ (B/\A) by XBOOLE_1:40 .=B by XBOOLE_1:51;
hence thesis by A1,A2;
end;
theorem
for P being compact non empty Subset of (TOP-REAL 2),
P1 being Subset of (TOP-REAL 2)|P
st P is_simple_closed_curve
& Upper_Arc(P) /\ P1={W-min(P),E-max(P)} & Upper_Arc(P) \/ P1=P
holds P1=Lower_Arc(P)
proof let P be compact non empty Subset of (TOP-REAL 2),
P1 be Subset of (TOP-REAL 2)|P;
assume A1: P is_simple_closed_curve
& Upper_Arc(P) /\ P1={W-min(P),E-max(P)} & Upper_Arc(P) \/ P1=P;
set B=Upper_Arc(P);
(B \/ P1 \B)\/ (B /\ P1) =(P1 \ B) \/ (P1/\B) by XBOOLE_1:40 .=P1 by
XBOOLE_1:51;
hence thesis by A1,Th66;
end;
theorem
for P being compact non empty Subset of (TOP-REAL 2),
P1 being Subset of (TOP-REAL 2)|P
st P is_simple_closed_curve
& P1 /\ Lower_Arc(P)={W-min(P),E-max(P)} & P1 \/ Lower_Arc(P)=P
holds P1=Upper_Arc(P)
proof let P be compact non empty Subset of (TOP-REAL 2),
P1 be Subset of (TOP-REAL 2)|P;
assume A1: P is_simple_closed_curve
& P1 /\ Lower_Arc(P)={W-min(P),E-max(P)} & P1 \/ Lower_Arc(P)=P;
set B=Lower_Arc(P);
(P1 \/ B\B) \/ (P1 /\ B)
=P1 /\B \/ (P1\B) by XBOOLE_1:40
.=P1 by XBOOLE_1:51;
hence thesis by A1,Th66;
end;
begin ::An Order of Points in a Simple Closed Curve
theorem Th69:
for P being Subset of TOP-REAL 2,
p1, p2, q being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 &
LE q,p1,P,p1,p2 holds q=p1
proof let P be Subset of TOP-REAL 2,
p1, p2, q be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2 & LE q,p1,P,p1,p2;
then q in P by JORDAN5C:def 3;
then LE p1,q,P,p1,p2 by A1,JORDAN5C:10;
hence q=p1 by A1,JORDAN5C:12;
end;
theorem Th70:
for P being Subset of TOP-REAL 2,
p1, p2, q being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 &
LE p2,q,P,p1,p2 holds q=p2
proof let P be Subset of TOP-REAL 2,
p1, p2, q be Point of TOP-REAL 2;
assume A1: P is_an_arc_of p1,p2 & LE p2,q,P,p1,p2;
then q in P by JORDAN5C:def 3;
then LE q,p2,P,p1,p2 by A1,JORDAN5C:10;
hence q=p2 by A1,JORDAN5C:12;
end;
definition
let P be compact non empty Subset of TOP-REAL 2,
q1,q2 be Point of TOP-REAL 2;
pred LE q1,q2,P means
:Def10: q1 in Upper_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P) or
q1 in Upper_Arc(P) & q2 in Upper_Arc(P) &
LE q1,q2,Upper_Arc(P),W-min(P),E-max(P) or
q1 in Lower_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P) &
LE q1,q2,Lower_Arc(P),E-max(P),W-min(P);
end;
theorem
for P being compact non empty Subset of (TOP-REAL 2),
q being Point of TOP-REAL 2
st P is_simple_closed_curve & q in P
holds LE q,q,P
proof let P be compact non empty Subset of (TOP-REAL 2),
q be Point of TOP-REAL 2;
assume A1: P is_simple_closed_curve & q in P;
then A2:Lower_Arc(P) is_an_arc_of E-max(P),W-min(P)
& Upper_Arc(P) /\ Lower_Arc(P)={W-min(P),E-max(P)}
& Upper_Arc(P) \/ Lower_Arc(P)=P
& First_Point(Upper_Arc(P),W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(Lower_Arc(P),E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2
by Def9;
A3: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,Th65;
now per cases by A1,A2,XBOOLE_0:def 2;
case A4:q in Upper_Arc(P);
then LE q,q,Upper_Arc(P),W-min(P),E-max(P) by A3,JORDAN5C:9;
hence LE q,q,P by A4,Def10;
case A5:q in Lower_Arc(P) & not q in Upper_Arc(P);
then A6:LE q,q,Lower_Arc(P),E-max(P),W-min(P) by A2,JORDAN5C:9;
q <> W-min P by A3,A5,TOPREAL1:4;
hence LE q,q,P by A5,A6,Def10;
end;
hence LE q,q,P;
end;
theorem
for P being compact non empty Subset of TOP-REAL 2,
q1,q2 being Point of TOP-REAL 2
st P is_simple_closed_curve & LE q1,q2,P & LE q2,q1,P
holds q1=q2
proof let P be compact non empty Subset of TOP-REAL 2,
q1,q2 be Point of TOP-REAL 2;
assume A1: P is_simple_closed_curve & LE q1,q2,P & LE q2,q1,P;
then A2: Lower_Arc(P) is_an_arc_of E-max(P),W-min(P)
& Upper_Arc(P) /\ Lower_Arc(P)={W-min(P),E-max(P)}
& Upper_Arc(P) \/ Lower_Arc(P)=P
& First_Point(Upper_Arc(P),W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(Lower_Arc(P),E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2 by Def9;
A3: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,Th65;
now per cases by A1,Def10;
case A4:q1 in Upper_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P);
now per cases by A1,Def10;
case A5: q2 in Upper_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P);
then q1 in Upper_Arc(P) /\ Lower_Arc(P) by A4,XBOOLE_0:def 3;
then A6:q1=E-max(P) by A2,A5,TARSKI:def 2;
q2 in Upper_Arc(P) /\ Lower_Arc(P) by A4,A5,XBOOLE_0:def 3;
hence q1=q2 by A2,A4,A6,TARSKI:def 2;
case A7: q2 in Upper_Arc(P) & q1 in Upper_Arc(P) &
LE q2,q1,Upper_Arc(P),W-min(P),E-max(P);
then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A4,XBOOLE_0:def 3;
then q2=E-max(P) by A2,A4,TARSKI:def 2;
hence q1=q2 by A3,A7,Th70;
case A8: q2 in Lower_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P) &
LE q2,q1,Lower_Arc(P),E-max(P),W-min(P);
then q1 in Upper_Arc(P) /\ Lower_Arc(P) by A4,XBOOLE_0:def 3;
then q1=E-max(P) by A2,A8,TARSKI:def 2;
hence q1=q2 by A2,A8,Th69;
end;
hence q1=q2;
case A9:q1 in Upper_Arc(P) & q2 in Upper_Arc(P)
& LE q1,q2,Upper_Arc(P),W-min(P),E-max(P);
now per cases by A1,Def10;
case A10: q2 in Upper_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P);
then q1 in Upper_Arc(P) /\ Lower_Arc(P) by A9,XBOOLE_0:def 3;
then q1=E-max(P) by A2,A10,TARSKI:def 2;
hence q1=q2 by A3,A9,Th70;
case q2 in Upper_Arc(P) & q1 in Upper_Arc(P) &
LE q2,q1,Upper_Arc(P),W-min(P),E-max(P);
hence q1=q2 by A3,A9,JORDAN5C:12;
case A11: q2 in Lower_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P) &
LE q2,q1,Lower_Arc(P),E-max(P),W-min(P);
then q1 in Upper_Arc(P) /\ Lower_Arc(P) by A9,XBOOLE_0:def 3;
then q1=E-max(P) by A2,A11,TARSKI:def 2;
hence q1=q2 by A2,A11,Th69;
end;
hence q1=q2;
case A12:q1 in Lower_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P) &
LE q1,q2,Lower_Arc(P),E-max(P),W-min(P);
now per cases by A1,Def10;
case q2 in Upper_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P);
then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A12,XBOOLE_0:def 3;
then q2=E-max(P) by A2,A12,TARSKI:def 2;
hence q1=q2 by A2,A12,Th69;
case A13: q2 in Upper_Arc(P) & q1 in Upper_Arc(P) &
LE q2,q1,Upper_Arc(P),W-min(P),E-max(P);
then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A12,XBOOLE_0:def 3;
then q2=E-max(P) by A2,A12,TARSKI:def 2;
hence q1=q2 by A3,A13,Th70;
case q2 in Lower_Arc(P) & q1 in Lower_Arc(P)& not q1=W-min(P) &
LE q2,q1,Lower_Arc(P),E-max(P),W-min(P);
hence q1=q2 by A2,A12,JORDAN5C:12;
end;
hence q1=q2;
end;
hence q1=q2;
end;
theorem
for P being compact non empty Subset of TOP-REAL 2,
q1,q2,q3 being Point of TOP-REAL 2
st P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P
holds LE q1,q3,P
proof let P be compact non empty Subset of TOP-REAL 2,
q1,q2,q3 be Point of TOP-REAL 2;
assume A1: P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P;
then A2: Lower_Arc(P) is_an_arc_of E-max(P),W-min(P)
& Upper_Arc(P) /\ Lower_Arc(P)={W-min(P),E-max(P)}
& Upper_Arc(P) \/ Lower_Arc(P)=P
& First_Point(Upper_Arc(P),W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
Last_Point(Lower_Arc(P),E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2 by Def9;
A3: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,Th65;
now per cases by A1,Def10;
case A4:q1 in Upper_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P);
now per cases by A1,Def10;
case q2 in Upper_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P);
hence LE q1,q3,P by A4,Def10;
case A5: q2 in Upper_Arc(P) & q3 in Upper_Arc(P) &
LE q2,q3,Upper_Arc(P),W-min(P),E-max(P);
then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A4,XBOOLE_0:def 3;
then q2=E-max(P) by A2,A4,TARSKI:def 2;
hence LE q1,q3,P by A1,A3,A5,Th70;
case q2 in Lower_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P) &
LE q2,q3,Lower_Arc(P),E-max(P),W-min(P);
hence LE q1,q3,P by A4,Def10;
end;
hence LE q1,q3,P;
case A6:q1 in Upper_Arc(P) & q2 in Upper_Arc(P)
& LE q1,q2,Upper_Arc(P),W-min(P),E-max(P);
now per cases by A1,Def10;
case q2 in Upper_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P);
hence LE q1,q3,P by A6,Def10;
case A7: q2 in Upper_Arc(P) & q3 in Upper_Arc(P) &
LE q2,q3,Upper_Arc(P),W-min(P),E-max(P);
then LE q1,q3,Upper_Arc(P),W-min(P),E-max(P) by A3,A6,JORDAN5C:13;
hence LE q1,q3,P by A6,A7,Def10;
case q2 in Lower_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P) &
LE q2,q3,Lower_Arc(P),E-max(P),W-min(P);
hence LE q1,q3,P by A6,Def10;
end;
hence LE q1,q3,P;
case A8:q1 in Lower_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P) &
LE q1,q2,Lower_Arc(P),E-max(P),W-min(P);
now per cases by A1,Def10;
case A9: q2 in Upper_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P);
then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A8,XBOOLE_0:def 3;
then q2=E-max(P) by A2,A8,TARSKI:def 2;
then LE q2,q3,Lower_Arc(P),E-max(P),W-min(P) by A2,A9,JORDAN5C:10;
then LE q1,q3,Lower_Arc(P),E-max(P),W-min(P) by A2,A8,JORDAN5C:13;
hence LE q1,q3,P by A8,A9,Def10;
case A10: q2 in Upper_Arc(P) & q3 in Upper_Arc(P) &
LE q2,q3,Upper_Arc(P),W-min(P),E-max(P);
then q2 in Upper_Arc(P) /\ Lower_Arc(P) by A8,XBOOLE_0:def 3;
then q2=E-max(P) by A2,A8,TARSKI:def 2;
hence LE q1,q3,P by A1,A3,A10,Th70;
case A11: q2 in Lower_Arc(P) & q3 in Lower_Arc(P)& not q3=W-min(P) &
LE q2,q3,Lower_Arc(P),E-max(P),W-min(P);
then LE q1,q3,Lower_Arc(P),E-max(P),W-min(P) by A2,A8,JORDAN5C:13;
hence LE q1,q3,P by A8,A11,Def10;
end;
hence LE q1,q3,P;
end;
hence LE q1,q3,P;
end;