let P be Subset of (); :: thesis: for p1, p2 being Point of () st P is_an_arc_of p1,p2 holds
ex q being Point of () st
( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 )

let p1, p2 be Point of (); :: thesis: ( P is_an_arc_of p1,p2 implies ex q being Point of () 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 () 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 () by ;
consider f being Function of I[01],(() | P9) such that
A3: f is being_homeomorphism and
A4: f . 0 = p1 and
A5: f . 1 = p2 by ;
A6: f is continuous by ;
consider h being Function of (),R^1 such that
A7: for p being Element of () holds h . p = p /. 1 by JORDAN2B:1;
1 in Seg 2 by FINSEQ_1:1;
then A8: h is continuous by ;
A9: the carrier of (() | P) = [#] (() | P)
.= P9 by PRE_TOPC:def 5 ;
then A10: f is Function of the carrier of I[01], the carrier of () by FUNCT_2:7;
reconsider f1 = f as Function of I[01],() by ;
A11: f1 is continuous by ;
reconsider g = h * f as Function of I[01],R^1 by A10;
A12: dom f = [.0,1.] by ;
then A13: 0 in dom f by XXREAL_1:1;
A14: 1 in dom f by ;
A15: g . 0 = h . (f . 0) by
.= p1 /. 1 by A4, A7
.= p1 `1 by JORDAN2B:29 ;
A16: g . 1 = h . (f . 1) by
.= 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 ; :: thesis: ex q being Point of () 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 ;
A20: r1 in [.0,1.] by ;
A21: r1 in the carrier of I[01] by ;
then reconsider q1 = f . r1 as Point of () by ;
g . r1 = h . (f . r1) by
.= q1 /. 1 by A7
.= q1 `1 by JORDAN2B:29 ;
hence ex q being Point of () st
( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 ) by ; :: thesis: verum
end;
suppose g . 0 = g . 1 ; :: thesis: ex q being Point of () st
( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 )

hence ex q being Point of () st
( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 ) by A2, A15, A16; :: thesis: verum
end;
end;