r by A7; p/.1>r by A10,JORDAN2B:29; hence thesis by A9; end; {p where p is Point of TOP-REAL 2: r

r by A12,JORDAN2B:29; hence thesis by A7,A11; end; then A13: P`={p where p is Point of TOP-REAL 2: r

=r;
{p where p is Element of TOP-REAL 2 : P[p]}
is Subset of TOP-REAL 2 from DOMAIN_1:sch 7;
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 Th4;
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 DOMAIN_1:sch 7;
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 Th5;
A4: P c= P1 /\ P2
proof
let x be object;
assume x in P;
then
A5: ex p being Point of TOP-REAL 2 st p=x & p`1=r by A1;
then
A6: x in P1;
x in P2 by A5;
hence thesis by A6,XBOOLE_0:def 4;
end;
P1 /\ P2 c= P
proof
let x be object;
assume
A7: x in P1 /\ P2;
then
A8: x in P1 by XBOOLE_0:def 4;
A9: x in P2 by A7,XBOOLE_0:def 4;
consider q1 being Point of TOP-REAL 2 such that
A10: q1=x and
A11: q1`1>=r by A8;
ex q2 being Point of TOP-REAL 2 st ( q2=x)&( q2`1<=r) by A9;
then q1`1=r by A10,A11,XXREAL_0:1;
hence thesis by A1,A10;
end;
then P=P1 /\ P2 by A4;
hence thesis by A2,A3,TOPS_1:8;
end;
theorem Th7:
for r being Real, 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, 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:1;
A3: P` c= {p where p is Point of TOP-REAL 2: p`2

r by A7; p/.2>r by A10,JORDAN2B:29; hence thesis by A9; end; {p where p is Point of TOP-REAL 2: r

r by A12,JORDAN2B:29; hence thesis by A7,A11; end; then A13: P`={p where p is Point of TOP-REAL 2: r

=r;
{p where p is Element of TOP-REAL 2 : P[p]}
is Subset of TOP-REAL 2 from DOMAIN_1:sch 7;
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 Th7;
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 DOMAIN_1:sch 7;
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 Th8;
A4: P c= P1 /\ P2
proof
let x be object;
assume x in P;
then
A5: ex p being Point of TOP-REAL 2 st ( p=x)&( p`2=r) by A1;
then
A6: x in P1;
x in P2 by A5;
hence thesis by A6,XBOOLE_0:def 4;
end;
P1 /\ P2 c= P
proof
let x be object;
assume
A7: x in P1 /\ P2;
then
A8: x in P1 by XBOOLE_0:def 4;
A9: x in P2 by A7,XBOOLE_0:def 4;
consider q1 being Point of TOP-REAL 2 such that
A10: q1=x and
A11: q1`2>=r by A8;
ex q2 being Point of TOP-REAL 2 st ( q2=x)&( q2`2<=r) by A9;
then q1`2=r by A10,A11,XXREAL_0:1;
hence thesis by A1,A10;
end;
then P=P1 /\ P2 by A4;
hence thesis by A2,A3,TOPS_1:8;
end;
theorem Th10:
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 Function of I[01], (TOP-REAL n)|P such that
A2: f is being_homeomorphism and f.0 = p1
and f.1 = p2 by TOPREAL1:def 1;
reconsider P9 = P as non empty Subset of TOP-REAL n by A1,TOPREAL1:1;
A3: f is continuous Function of I[01],(TOP-REAL n)|P9 by A2,TOPS_2:def 5;
A4: [#]I[01] is connected by CONNSP_1:27,TREAL_1:19;
A5: rng f=[#]((TOP-REAL n)|P) by A2,TOPS_2:def 5;
A6: [#]((TOP-REAL n)|P)=P by PRE_TOPC:def 5;
dom f=[#]I[01] by A2,TOPS_2:def 5;
then
A7: P=f.:([#]I[01]) by A5,A6,RELAT_1:113;
f.:([#]I[01]) is connected by A3,A4,TOPS_2:61;
hence thesis by A7,CONNSP_1:23;
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 P is closed
by COMPTS_1:7,JORDAN5A:1;
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
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:1;
reconsider P9 = P as non empty Subset of TOP-REAL 2 by A1,TOPREAL1:1;
consider f being Function of I[01], (TOP-REAL 2)|P9 such that
A3: f is being_homeomorphism and
A4: f.0 = p1 and
A5: f.1 = p2 by A1,TOPREAL1:def 1;
A6: f is continuous by A3,TOPS_2:def 5;
consider h being Function of TOP-REAL 2,R^1 such that
A7: for p being Element of TOP-REAL 2 holds h.p=p/.1 by JORDAN2B:1;
1 in Seg 2 by FINSEQ_1:1;
then
A8: h is continuous by A7,JORDAN2B:18;
A9: the carrier of (TOP-REAL 2)|P = [#]((TOP-REAL 2)|P)
.=P9 by PRE_TOPC:def 5;
then
A10: f is Function of the carrier of I[01],the carrier of TOP-REAL 2
by FUNCT_2:7;
reconsider f1=f as Function of I[01],TOP-REAL 2 by A9,FUNCT_2:7;
A11: f1 is continuous by A6,Th3;
reconsider g= h*f as Function of I[01],R^1 by A10;
A12: dom f=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
then
A13: 0 in dom f by XXREAL_1:1;
A14: 1 in dom f by A12,XXREAL_1:1;
A15: g.0 =h.(f.0) by A13,FUNCT_1:13
.=p1/.1 by A4,A7
.=p1`1 by JORDAN2B:29;
A16: g.1 =h.(f.1) by A14,FUNCT_1:13
.=p2/.1 by A5,A7
.=p2`1 by JORDAN2B:29;
per cases;
suppose g.0<>g.1;
then consider r1 being Real such that
A17: 0~~0 by XREAL_1:50;
then consider r be Real such that
A32: r in P5 and
A33: r~~