let P be Subset of (); :: thesis: for p1, p2 being Point of () st P is_an_arc_of p1,p2 holds
( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 )

let p1, p2 be Point of (); :: thesis: ( P is_an_arc_of p1,p2 implies ( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 ) )
assume A1: P is_an_arc_of p1,p2 ; :: thesis: ( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 )
A2: now :: thesis: ( p1 = y_Middle (P,p1,p2) implies p1 `2 = p2 `2 )
assume A3: p1 = y_Middle (P,p1,p2) ; :: thesis: p1 `2 = p2 `2
deffunc H1( Point of ()) -> Point of () = \$1;
defpred S1[ Point of ()] means \$1 `2 = ((p1 `2) + (p2 `2)) / 2;
reconsider Q1 = { H1(q) where q is Point of () : S1[q] } as Subset of () from A4: P meets Q1 by ;
A5: P /\ Q1 is closed by ;
y_Middle (P,p1,p2) = First_Point (P,p1,p2,Q1) by Def2;
then p1 in P /\ Q1 by ;
then p1 in Q1 by XBOOLE_0:def 4;
then ex q being Point of () st
( q = p1 & q `2 = ((p1 `2) + (p2 `2)) / 2 ) ;
hence p1 `2 = p2 `2 ; :: thesis: verum
end;
now :: thesis: ( p1 `2 = p2 `2 implies p1 = y_Middle (P,p1,p2) )
assume A6: p1 `2 = p2 `2 ; :: thesis: p1 = y_Middle (P,p1,p2)
for Q being Subset of () st Q = { q where q is Point of () : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds
p1 = First_Point (P,p1,p2,Q)
proof
let Q be Subset of (); :: thesis: ( Q = { q where q is Point of () : q `2 = ((p1 `2) + (p2 `2)) / 2 } implies p1 = First_Point (P,p1,p2,Q) )
assume A7: Q = { q where q is Point of () : q `2 = ((p1 `2) + (p2 `2)) / 2 } ; :: thesis: p1 = First_Point (P,p1,p2,Q)
then A8: p1 in Q by A6;
P /\ Q is closed by A1, A7, Th14;
hence p1 = First_Point (P,p1,p2,Q) by ; :: thesis: verum
end;
hence p1 = y_Middle (P,p1,p2) by Def2; :: thesis: verum
end;
hence ( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 ) by A2; :: thesis: verum