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_{1}( Point of (TOP-REAL 2)) -> Point of (TOP-REAL 2) = $1;

defpred S_{1}[ Point of (TOP-REAL 2)] means $1 `1 = ((p1 `1) + (p2 `1)) / 2;

reconsider Q = { H_{1}(q) where q is Point of (TOP-REAL 2) : S_{1}[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_{2}[ Point of (TOP-REAL 2)] means $1 `2 = ((p1 `2) + (p2 `2)) / 2;

reconsider Q2 = { H_{1}(q) where q is Point of (TOP-REAL 2) : S_{2}[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

( 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

defpred S

reconsider Q = { H

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

reconsider Q2 = { H

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