let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
( x_Middle P,p1,p2 in P & y_Middle P,p1,p2 in P )
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 implies ( x_Middle P,p1,p2 in P & y_Middle P,p1,p2 in P ) )
assume A1: P is_an_arc_of p1,p2 ; :: thesis: ( x_Middle P,p1,p2 in P & y_Middle P,p1,p2 in P )
deffunc H₁( Point of (TOP-REAL 2)) -> Point of (TOP-REAL 2) = $1;
defpred S₁[ Point of (TOP-REAL 2)] means $1 `1 = ((p1 `1 ) + (p2 `1 )) / 2;
reconsider Q = { H<sub>1</sub>(q) where q is Point of (TOP-REAL 2) : S<sub>1</sub>[q] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch 8();
A2: x_Middle P,p1,p2 = First_Point P,p1,p2,Q by Def1;
( P meets Q & P /\ Q is closed ) by A1, Th14;
then A3: x_Middle P,p1,p2 in P /\ Q by A1, A2, JORDAN5C:def 1;
defpred S<sub>2</sub>[ Point of (TOP-REAL 2)] means $1 `2 = ((p1 `2 ) + (p2 `2 )) / 2;
reconsider Q2 = { H₁(q) where q is Point of (TOP-REAL 2) : S₂[q] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch 8();
A4: y_Middle P,p1,p2 = First_Point P,p1,p2,Q2 by Def2;
( P meets Q2 & P /\ Q2 is closed ) by A1, Th15;
then y_Middle P,p1,p2 in P /\ Q2 by A1, A4, JORDAN5C:def 1;
hence ( x_Middle P,p1,p2 in P & y_Middle P,p1,p2 in P ) by A3, XBOOLE_0:def 4; :: thesis: verum