let P be Subset of (TOP-REAL 2); for 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 )
let p1, p2 be Point of (TOP-REAL 2); ( P is_an_arc_of p1,p2 implies ex q being Point of (TOP-REAL 2) st
( q in P & q `1 = ((p1 `1 ) + (p2 `1 )) / 2 ) )
assume A1:
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 )
then A2:
p1 in P
by TOPREAL1:4;
reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:4;
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 2;
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:3;
then A8:
h is continuous
by A7, JORDAN2B:22;
A9: the carrier of ((TOP-REAL 2) | P) =
[#] ((TOP-REAL 2) | P)
.=
P9
by PRE_TOPC:def 10
;
then A10:
f is Function of the carrier of I[01] ,the carrier of (TOP-REAL 2)
by FUNCT_2:9;
reconsider f1 = f as Function of I[01] ,(TOP-REAL 2) by A9, FUNCT_2:9;
A11:
f1 is continuous
by A6, Th4;
reconsider g = h * f as Function of I[01] ,R^1 by A10;
A12:
dom f = [.0 ,1.]
by BORSUK_1:83, 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:23
.=
p1 /. 1
by A4, A7
.=
p1 `1
by JORDAN2B:35
;
A16: g . 1 =
h . (f . 1)
by A14, FUNCT_1:23
.=
p2 /. 1
by A5, A7
.=
p2 `1
by JORDAN2B:35
;
per cases
( g . 0 <> g . 1 or g . 0 = g . 1 )
;
suppose
g . 0 <> g . 1
;
ex q being Point of (TOP-REAL 2) st
( q in P & q `1 = ((p1 `1 ) + (p2 `1 )) / 2 )then consider r1 being
Real such that A17:
0 < r1
and A18:
r1 < 1
and A19:
g . r1 = ((p1 `1 ) + (p2 `1 )) / 2
by A8, A11, A15, A16, TOPREAL5:15;
A20:
r1 in [.0 ,1.]
by A17, A18, XXREAL_1:1;
A21:
r1 in the
carrier of
I[01]
by A17, A18, BORSUK_1:83, XXREAL_1:1;
then reconsider q1 =
f . r1 as
Point of
(TOP-REAL 2) by A10, FUNCT_2:7;
g . r1 =
h . (f . r1)
by A12, A20, FUNCT_1:23
.=
q1 /. 1
by A7
.=
q1 `1
by JORDAN2B:35
;
hence
ex
q being
Point of
(TOP-REAL 2) st
(
q in P &
q `1 = ((p1 `1 ) + (p2 `1 )) / 2 )
by A9, A19, A21, FUNCT_2:7;
verum end;