let P be non empty Subset of (TOP-REAL 2); 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); ( P is_an_arc_of p1,p2 implies Segment (P,p1,p2,p1,p2) = P )
assume
P is_an_arc_of p1,p2
; 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; verum