let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, p being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & p in P holds
Segment P,p1,p2,p,p = {p}
let p1, p2, p be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & p in P implies Segment P,p1,p2,p,p = {p} )
assume that
A1: P is_an_arc_of p1,p2 and
A2: p in P ; :: thesis: Segment P,p1,p2,p,p = {p}
A3: Segment P,p1,p2,p,p = { q where q is Point of (TOP-REAL 2) : ( LE p,q,P,p1,p2 & LE q,p,P,p1,p2 ) } by JORDAN6:29;
A4: {p} c= Segment P,p1,p2,p,p

proof

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

end;

Segment P,p1,p2,p,p c= {p}

proof

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

end;

hence Segment P,p1,p2,p,p = {p} by A4, XBOOLE_0:def 10; :: thesis: verum