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

let p1, p2 be Point of (); :: thesis: ( P is_an_arc_of p1,p2 & Q = { q where q is Point of () : q `1 = ((p1 `1) + (p2 `1)) / 2 } implies ( P meets Q & P /\ Q is closed ) )
reconsider W = P as Subset of () ;
assume A1: ( P is_an_arc_of p1,p2 & Q = { q where q is Point of () : q `1 = ((p1 `1) + (p2 `1)) / 2 } ) ; :: thesis: ( P meets Q & P /\ Q is closed )
consider f being Function of (),R^1 such that
A2: for p being Element of () holds f . p = p /. 1 by JORDAN2B:1;
reconsider P9 = P as non empty Subset of () by ;
A3: 1 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 /. 1 by A2
.= p1 `1 by JORDAN2B:29 ;
A11: g . p29 = f . p2 by
.= p2 /. 1 by A2
.= p2 `1 by JORDAN2B:29 ;
W is connected by ;
then A12: (TOP-REAL 2) | P is connected by CONNSP_1:def 3;
A13: now :: thesis: ( ( p1 `1 <= p2 `1 & P meets Q ) or ( p1 `1 > p2 `1 & P meets Q ) )
per cases ( p1 `1 <= p2 `1 or p1 `1 > p2 `1 ) ;
case A14: p1 `1 <= p2 `1 ; :: thesis: P meets Q
then A15: p1 `1 <= ((p1 `1) + (p2 `1)) / 2 by Th1;
((p1 `1) + (p2 `1)) / 2 <= p2 `1 by ;
then consider xc being Point of (() | P) such that
A16: g . xc = ((p1 `1) + (p2 `1)) / 2 by ;
xc in P by A6;
then reconsider pc = xc as Point of () ;
g . xc = f . xc by
.= pc /. 1 by A2
.= pc `1 by JORDAN2B:29 ;
then xc in Q by ;
hence P meets Q by ; :: thesis: verum
end;
case A17: p1 `1 > p2 `1 ; :: thesis: P meets Q
then A18: p2 `1 <= ((p1 `1) + (p2 `1)) / 2 by Th1;
((p1 `1) + (p2 `1)) / 2 <= p1 `1 by ;
then consider xc being Point of (() | P) such that
A19: g . xc = ((p1 `1) + (p2 `1)) / 2 by ;
xc in P by A6;
then reconsider pc = xc as Point of () ;
g . xc = f . xc by
.= pc /. 1 by A2
.= pc `1 by JORDAN2B:29 ;
then xc in Q by ;
hence P meets Q by ; :: thesis: verum
end;
end;
end;
reconsider P1 = P, Q1 = Q as Subset of () ;
A20: P1 is closed by ;
Q1 is closed by ;
hence ( P meets Q & P /\ Q is closed ) by ; :: thesis: verum