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:26;
A4: {p} c= Segment (P,p1,p2,p,p)

proof

let x be object ; :: 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 object ; :: 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