let P be non empty Subset of (TOP-REAL 2); :: thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
Segment P,p1,p2,p1,p2 = P
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 implies Segment P,p1,p2,p1,p2 = P )
assume P is_an_arc_of p1,p2 ; :: thesis: Segment P,p1,p2,p1,p2 = P
then A1: ( R_Segment P,p1,p2,p1 = P & L_Segment P,p1,p2,p2 = P ) by JORDAN6:25, JORDAN6:27;
(R_Segment P,p1,p2,p1) /\ (L_Segment P,p1,p2,p2) = Segment P,p1,p2,p1,p2 by JORDAN6:def 5;
hence Segment P,p1,p2,p1,p2 = P by A1; :: thesis: verum