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

( P meets Q1 & P /\ Q1 is closed )

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & Q1 = { q where q is Point of (TOP-REAL 2) : 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 (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } ) ; :: thesis: ( P meets Q1 & P /\ Q1 is closed )

consider f being Function of (TOP-REAL 2),R^1 such that

A2: for p being Element of (TOP-REAL 2) holds f . p = p /. 2 by JORDAN2B:1;

reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1;

A3: 2 in Seg 2 by FINSEQ_1:1;

A4: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;

A5: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def 5;

then A6: the carrier of ((TOP-REAL 2) | P9) = P9 ;

A7: dom (f | P) = the carrier of (TOP-REAL 2) /\ P by A4, RELAT_1:61

.= P by XBOOLE_1:28 ;

rng (f | P) c= the carrier of R^1 ;

then reconsider g = f | P as Function of ((TOP-REAL 2) | P),R^1 by A5, A7, FUNCT_2:def 1, RELSET_1:4;

reconsider g = g as continuous Function of ((TOP-REAL 2) | P9),R^1 by A2, A3, JORDAN2B:18, TOPMETR:7;

A8: p1 in P by A1, TOPREAL1:1;

A9: p2 in P by A1, TOPREAL1:1;

reconsider p19 = p1, p29 = p2 as Point of ((TOP-REAL 2) | P) by A1, A5, TOPREAL1:1;

A10: g . p19 = f . p1 by A8, FUNCT_1:49

.= p1 /. 2 by A2

.= p1 `2 by JORDAN2B:29 ;

A11: g . p29 = f . p2 by A9, FUNCT_1:49

.= p2 /. 2 by A2

.= p2 `2 by JORDAN2B:29 ;

reconsider W = P as Subset of (TOP-REAL 2) ;

W is connected by A1, Th10;

then A12: (TOP-REAL 2) | P is connected by CONNSP_1:def 3;

A20: P1 is closed by A1, COMPTS_1:7, JORDAN5A:1;

Q2 is closed by A1, Th9;

hence ( P meets Q1 & P /\ Q1 is closed ) by A13, A20, TOPS_1:8; :: thesis: verum

( P meets Q1 & P /\ Q1 is closed )

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & Q1 = { q where q is Point of (TOP-REAL 2) : 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 (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } ) ; :: thesis: ( P meets Q1 & P /\ Q1 is closed )

consider f being Function of (TOP-REAL 2),R^1 such that

A2: for p being Element of (TOP-REAL 2) holds f . p = p /. 2 by JORDAN2B:1;

reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1;

A3: 2 in Seg 2 by FINSEQ_1:1;

A4: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;

A5: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def 5;

then A6: the carrier of ((TOP-REAL 2) | P9) = P9 ;

A7: dom (f | P) = the carrier of (TOP-REAL 2) /\ P by A4, RELAT_1:61

.= P by XBOOLE_1:28 ;

rng (f | P) c= the carrier of R^1 ;

then reconsider g = f | P as Function of ((TOP-REAL 2) | P),R^1 by A5, A7, FUNCT_2:def 1, RELSET_1:4;

reconsider g = g as continuous Function of ((TOP-REAL 2) | P9),R^1 by A2, A3, JORDAN2B:18, TOPMETR:7;

A8: p1 in P by A1, TOPREAL1:1;

A9: p2 in P by A1, TOPREAL1:1;

reconsider p19 = p1, p29 = p2 as Point of ((TOP-REAL 2) | P) by A1, A5, TOPREAL1:1;

A10: g . p19 = f . p1 by A8, FUNCT_1:49

.= p1 /. 2 by A2

.= p1 `2 by JORDAN2B:29 ;

A11: g . p29 = f . p2 by A9, FUNCT_1:49

.= p2 /. 2 by A2

.= p2 `2 by JORDAN2B:29 ;

reconsider W = P as Subset of (TOP-REAL 2) ;

W is connected by A1, Th10;

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 ) )end;

reconsider P1 = P, Q2 = Q1 as Subset of (TOP-REAL 2) ;per cases
( p1 `2 <= p2 `2 or p1 `2 > p2 `2 )
;

end;

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 A14, Th1;

then consider xc being Point of ((TOP-REAL 2) | P) such that

A16: g . xc = ((p1 `2) + (p2 `2)) / 2 by A10, A11, A12, A15, TOPREAL5:4;

xc in P by A6;

then reconsider pc = xc as Point of (TOP-REAL 2) ;

g . xc = f . xc by A5, FUNCT_1:49

.= pc /. 2 by A2

.= pc `2 by JORDAN2B:29 ;

then xc in Q1 by A1, A16;

hence P meets Q1 by A6, XBOOLE_0:3; :: thesis: verum

end;((p1 `2) + (p2 `2)) / 2 <= p2 `2 by A14, Th1;

then consider xc being Point of ((TOP-REAL 2) | P) such that

A16: g . xc = ((p1 `2) + (p2 `2)) / 2 by A10, A11, A12, A15, TOPREAL5:4;

xc in P by A6;

then reconsider pc = xc as Point of (TOP-REAL 2) ;

g . xc = f . xc by A5, FUNCT_1:49

.= pc /. 2 by A2

.= pc `2 by JORDAN2B:29 ;

then xc in Q1 by A1, A16;

hence P meets Q1 by A6, XBOOLE_0:3; :: thesis: verum

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 A17, Th1;

then consider xc being Point of ((TOP-REAL 2) | P) such that

A19: g . xc = ((p1 `2) + (p2 `2)) / 2 by A10, A11, A12, A18, TOPREAL5:4;

xc in P by A6;

then reconsider pc = xc as Point of (TOP-REAL 2) ;

g . xc = f . xc by A5, FUNCT_1:49

.= pc /. 2 by A2

.= pc `2 by JORDAN2B:29 ;

then xc in Q1 by A1, A19;

hence P meets Q1 by A6, XBOOLE_0:3; :: thesis: verum

end;((p1 `2) + (p2 `2)) / 2 <= p1 `2 by A17, Th1;

then consider xc being Point of ((TOP-REAL 2) | P) such that

A19: g . xc = ((p1 `2) + (p2 `2)) / 2 by A10, A11, A12, A18, TOPREAL5:4;

xc in P by A6;

then reconsider pc = xc as Point of (TOP-REAL 2) ;

g . xc = f . xc by A5, FUNCT_1:49

.= pc /. 2 by A2

.= pc `2 by JORDAN2B:29 ;

then xc in Q1 by A1, A19;

hence P meets Q1 by A6, XBOOLE_0:3; :: thesis: verum

A20: P1 is closed by A1, COMPTS_1:7, JORDAN5A:1;

Q2 is closed by A1, Th9;

hence ( P meets Q1 & P /\ Q1 is closed ) by A13, A20, TOPS_1:8; :: thesis: verum