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;
A3: P meets Q by A1, Th13;
P /\ Q is closed by A1, Th13;
then A4: x_Middle (P,p1,p2) in P /\ Q by A1, A2, A3, 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();
A5: y_Middle (P,p1,p2) = First_Point (P,p1,p2,Q2) by Def2;
A6: P meets Q2 by A1, Th14;
P /\ Q2 is closed by A1, Th14;
then y_Middle (P,p1,p2) in P /\ Q2 by A1, A5, A6, JORDAN5C:def 1;
hence ( x_Middle (P,p1,p2) in P & y_Middle (P,p1,p2) in P ) by A4, XBOOLE_0:def 4; :: thesis: verum