let P be Subset of (); :: thesis: for p1, p2 being Point of () 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 (); :: 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 H1( Point of ()) -> Point of () = \$1;
defpred S1[ Point of ()] means \$1 `1 = ((p1 `1) + (p2 `1)) / 2;
reconsider Q = { H1(q) where q is Point of () : S1[q] } as Subset of () from A2: x_Middle (P,p1,p2) = First_Point (P,p1,p2,Q) by Def1;
A3: P meets Q by ;
P /\ Q is closed by ;
then A4: x_Middle (P,p1,p2) in P /\ Q by ;
defpred S2[ Point of ()] means \$1 `2 = ((p1 `2) + (p2 `2)) / 2;
reconsider Q2 = { H1(q) where q is Point of () : S2[q] } as Subset of () from A5: y_Middle (P,p1,p2) = First_Point (P,p1,p2,Q2) by Def2;
A6: P meets Q2 by ;
P /\ Q2 is closed by ;
then y_Middle (P,p1,p2) in P /\ Q2 by ;
hence ( x_Middle (P,p1,p2) in P & y_Middle (P,p1,p2) in P ) by ; :: thesis: verum