let P, Q1 be Subset of (); :: thesis: for p1, p2 being Point of () st P is_an_arc_of p1,p2 & Q1 = { q where q is Point of () : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
( P meets Q1 & P /\ Q1 is closed )

let p1, p2 be Point of (); :: thesis: ( P is_an_arc_of p1,p2 & Q1 = { q where q is Point of () : q `2 = ((p1 `2) + (p2 `2)) / 2 } implies ( P meets Q1 & P /\ Q1 is closed ) )
assume A1: ( P is_an_arc_of p1,p2 & Q1 = { q where q is Point of () : q `2 = ((p1 `2) + (p2 `2)) / 2 } ) ; :: thesis: ( P meets Q1 & P /\ Q1 is closed )
consider f being Function of (),R^1 such that
A2: for p being Element of () holds f . p = p /. 2 by JORDAN2B:1;
reconsider P9 = P as non empty Subset of () by ;
A3: 2 in Seg 2 by FINSEQ_1:1;
A4: dom f = the carrier of () by FUNCT_2:def 1;
A5: [#] (() | P) = P by PRE_TOPC:def 5;
then A6: the carrier of (() | P9) = P9 ;
A7: dom (f | P) = the carrier of () /\ P by
.= P by XBOOLE_1:28 ;
rng (f | P) c= the carrier of R^1 ;
then reconsider g = f | P as Function of (() | P),R^1 by ;
reconsider g = g as continuous Function of (() | P9),R^1 by ;
A8: p1 in P by ;
A9: p2 in P by ;
reconsider p19 = p1, p29 = p2 as Point of (() | P) by ;
A10: g . p19 = f . p1 by
.= p1 /. 2 by A2
.= p1 `2 by JORDAN2B:29 ;
A11: g . p29 = f . p2 by
.= p2 /. 2 by A2
.= p2 `2 by JORDAN2B:29 ;
reconsider W = P as Subset of () ;
W is connected by ;
then A12: (TOP-REAL 2) | P is connected by CONNSP_1:def 3;
A13: now :: thesis: ( ( p1 `2 <= p2 `2 & P meets Q1 ) or ( p1 `2 > p2 `2 & P meets Q1 ) )
per cases ( p1 `2 <= p2 `2 or p1 `2 > p2 `2 ) ;
case A14: p1 `2 <= p2 `2 ; :: thesis: P meets Q1
then A15: p1 `2 <= ((p1 `2) + (p2 `2)) / 2 by Th1;
((p1 `2) + (p2 `2)) / 2 <= p2 `2 by ;
then consider xc being Point of (() | P) such that
A16: g . xc = ((p1 `2) + (p2 `2)) / 2 by ;
xc in P by A6;
then reconsider pc = xc as Point of () ;
g . xc = f . xc by
.= pc /. 2 by A2
.= pc `2 by JORDAN2B:29 ;
then xc in Q1 by ;
hence P meets Q1 by ; :: thesis: verum
end;
case A17: p1 `2 > p2 `2 ; :: thesis: P meets Q1
then A18: p2 `2 <= ((p1 `2) + (p2 `2)) / 2 by Th1;
((p1 `2) + (p2 `2)) / 2 <= p1 `2 by ;
then consider xc being Point of (() | P) such that
A19: g . xc = ((p1 `2) + (p2 `2)) / 2 by ;
xc in P by A6;
then reconsider pc = xc as Point of () ;
g . xc = f . xc by
.= pc /. 2 by A2
.= pc `2 by JORDAN2B:29 ;
then xc in Q1 by ;
hence P meets Q1 by ; :: thesis: verum
end;
end;
end;
reconsider P1 = P, Q2 = Q1 as Subset of () ;
A20: P1 is closed by ;
Q2 is closed by ;
hence ( P meets Q1 & P /\ Q1 is closed ) by ; :: thesis: verum