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

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

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } implies ( P meets Q & P /\ Q is closed ) )

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

assume A1: ( P is_an_arc_of p1,p2 & Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } ) ; :: thesis: ( P meets Q & P /\ Q 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 /. 1 by JORDAN2B:1;

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

A3: 1 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 /. 1 by A2

.= p1 `1 by JORDAN2B:29 ;

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

.= p2 /. 1 by A2

.= p2 `1 by JORDAN2B:29 ;

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;

Q1 is closed by A1, Th6;

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

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

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } implies ( P meets Q & P /\ Q is closed ) )

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

assume A1: ( P is_an_arc_of p1,p2 & Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } ) ; :: thesis: ( P meets Q & P /\ Q 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 /. 1 by JORDAN2B:1;

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

A3: 1 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 /. 1 by A2

.= p1 `1 by JORDAN2B:29 ;

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

.= p2 /. 1 by A2

.= p2 `1 by JORDAN2B:29 ;

W is connected by A1, Th10;

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

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

end;

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

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

A16: g . xc = ((p1 `1) + (p2 `1)) / 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 /. 1 by A2

.= pc `1 by JORDAN2B:29 ;

then xc in Q by A1, A16;

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

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

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

A16: g . xc = ((p1 `1) + (p2 `1)) / 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 /. 1 by A2

.= pc `1 by JORDAN2B:29 ;

then xc in Q by A1, A16;

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

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

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

A19: g . xc = ((p1 `1) + (p2 `1)) / 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 /. 1 by A2

.= pc `1 by JORDAN2B:29 ;

then xc in Q by A1, A19;

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

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

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

A19: g . xc = ((p1 `1) + (p2 `1)) / 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 /. 1 by A2

.= pc `1 by JORDAN2B:29 ;

then xc in Q by A1, A19;

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

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

Q1 is closed by A1, Th6;

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