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
( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 )
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 implies ( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 ) )
assume A1: P is_an_arc_of p1,p2 ; :: thesis: ( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 )

A2: now :: thesis: ( p1 = x_Middle (P,p1,p2) implies p1 `1 = p2 `1 )

assume A3: p1 = x_Middle (P,p1,p2) ; :: thesis: p1 `1 = p2 `1
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 Q1 = { 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();
A4: P meets Q1 by A1, Th13;
A5: P /\ Q1 is closed by A1, Th13;
x_Middle (P,p1,p2) = First_Point (P,p1,p2,Q1) by Def1;
then p1 in P /\ Q1 by A1, A3, A4, A5, JORDAN5C:def 1;
then p1 in Q1 by XBOOLE_0:def 4;
then ex q being Point of (TOP-REAL 2) st
( q = p1 & q `1 = ((p1 `1) + (p2 `1)) / 2 ) ;
hence p1 `1 = p2 `1 ; :: thesis: verum

end;

now :: thesis: ( p1 `1 = p2 `1 implies p1 = x_Middle (P,p1,p2) )

assume A6: p1 `1 = p2 `1 ; :: thesis: p1 = x_Middle (P,p1,p2)
for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds
p1 = First_Point (P,p1,p2,Q)

proof

let Q be Subset of (TOP-REAL 2); :: thesis: ( Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } implies p1 = First_Point (P,p1,p2,Q) )
assume A7: Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } ; :: thesis: p1 = First_Point (P,p1,p2,Q)
then A8: p1 in Q by A6;
P /\ Q is closed by A1, A7, Th13;
hence p1 = First_Point (P,p1,p2,Q) by A1, A8, JORDAN5C:3; :: thesis: verum

end;

hence p1 = x_Middle (P,p1,p2) by Def1; :: thesis: verum

end;

hence ( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 ) by A2; :: thesis: verum