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 = Proj p,2
by JORDAN2B:1;
reconsider P' = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:4;
2 in Seg 2
by FINSEQ_1:3;
then A3:
f is continuous
by A2, JORDAN2B:22;
A4:
dom f = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
A5:
[#] ((TOP-REAL 2) | P) = P
by PRE_TOPC:def 10;
then A6:
the carrier of ((TOP-REAL 2) | P') = P'
;
A7: dom (f | P) =
the carrier of (TOP-REAL 2) /\ P
by A4, RELAT_1:90
.=
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:11;
reconsider g = g as continuous Function of ((TOP-REAL 2) | P'),R^1 by A3, TOPMETR:10;
A8:
( p1 in P & p2 in P )
by A1, TOPREAL1:4;
reconsider p1' = p1, p2' = p2 as Point of ((TOP-REAL 2) | P) by A1, A5, TOPREAL1:4;
A9: g . p1' =
f . p1
by A8, FUNCT_1:72
.=
Proj p1,2
by A2
.=
p1 `2
by JORDAN2B:35
;
A10: g . p2' =
f . p2
by A8, FUNCT_1:72
.=
Proj p2,2
by A2
.=
p2 `2
by JORDAN2B:35
;
reconsider W = P as Subset of (TOP-REAL 2) ;
W is connected
by A1, Th11;
then A11:
(TOP-REAL 2) | P is connected
by CONNSP_1:def 3;
reconsider P1 = P, Q2 = Q1 as Subset of (TOP-REAL 2) ;
A15:
P1 is closed
by A1, COMPTS_1:16, JORDAN5A:1;
Q2 is closed
by A1, Th10;
hence
( P meets Q1 & P /\ Q1 is closed )
by A12, A15, TOPS_1:35; :: thesis: verum