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: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
( 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:9;
A20:
r1 in [.0,1.]
by A17, A18, XXREAL_1:1;
A21:
r1 in the
carrier of
I[01]
by A17, A18, BORSUK_1:40, XXREAL_1:1;
then reconsider q1 =
f . r1 as
Point of
(TOP-REAL 2) by A10, FUNCT_2:5;
g . r1 =
h . (f . r1)
by A12, A20, FUNCT_1:13
.=
q1 /. 1
by A7
.=
q1 `1
by JORDAN2B:29
;
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:5;
verum end;