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,p1) = {p1}
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 implies L_Segment (P,p1,p2,p1) = {p1} )
assume A1: P is_an_arc_of p1,p2 ; :: thesis: L_Segment (P,p1,p2,p1) = {p1}
then A2: p1 in P by TOPREAL1:1;
thus L_Segment (P,p1,p2,p1) c= {p1} :: according to XBOOLE_0:def 10 :: thesis: {p1} c= L_Segment (P,p1,p2,p1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L_Segment (P,p1,p2,p1) or x in {p1} )
assume x in L_Segment (P,p1,p2,p1) ; :: thesis: x in {p1}
then consider q being Point of (TOP-REAL 2) such that
A3: q = x and
A4: LE q,p1,P,p1,p2 ;
q in P by A4;
then LE p1,q,P,p1,p2 by A1, JORDAN5C:10;
then q = p1 by A1, A4, JORDAN5C:12;
hence x in {p1} by A3, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {p1} or x in L_Segment (P,p1,p2,p1) )
assume x in {p1} ; :: thesis: x in L_Segment (P,p1,p2,p1)
then A5: x = p1 by TARSKI:def 1;
LE p1,p1,P,p1,p2 by A2, JORDAN5C:9;
hence x in L_Segment (P,p1,p2,p1) by A5; :: thesis: verum