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

L_Segment (P,p1,p2,p2) = P

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 implies L_Segment (P,p1,p2,p2) = P )

assume A1: P is_an_arc_of p1,p2 ; :: thesis: L_Segment (P,p1,p2,p2) = P

thus L_Segment (P,p1,p2,p2) c= P by Th19; :: according to XBOOLE_0:def 10 :: thesis: P c= L_Segment (P,p1,p2,p2)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in L_Segment (P,p1,p2,p2) )

assume A2: x in P ; :: thesis: x in L_Segment (P,p1,p2,p2)

then reconsider p = x as Point of (TOP-REAL 2) ;

LE p,p2,P,p1,p2 by A1, A2, JORDAN5C:10;

hence x in L_Segment (P,p1,p2,p2) ; :: thesis: verum

L_Segment (P,p1,p2,p2) = P

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 implies L_Segment (P,p1,p2,p2) = P )

assume A1: P is_an_arc_of p1,p2 ; :: thesis: L_Segment (P,p1,p2,p2) = P

thus L_Segment (P,p1,p2,p2) c= P by Th19; :: according to XBOOLE_0:def 10 :: thesis: P c= L_Segment (P,p1,p2,p2)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in L_Segment (P,p1,p2,p2) )

assume A2: x in P ; :: thesis: x in L_Segment (P,p1,p2,p2)

then reconsider p = x as Point of (TOP-REAL 2) ;

LE p,p2,P,p1,p2 by A1, A2, JORDAN5C:10;

hence x in L_Segment (P,p1,p2,p2) ; :: thesis: verum