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:22, JORDAN6:24;
(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