let P be Subset of (TOP-REAL 2); :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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 ;

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); :: thesis: ( 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 ; :: thesis: 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 )
;

end;

suppose
g . 0 <> g . 1
; :: thesis: ex q being Point of (TOP-REAL 2) st

( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 )

( 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; :: thesis: verum

end;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; :: thesis: verum