let P, Q be Subset of (TOP-REAL 2); 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); ( 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 } )
; ( 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
by RELAT_1:def 19;
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;
reconsider P1 = P, Q1 = Q as Subset of (TOP-REAL 2) ;
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; verum