theorem
for
P being non
empty Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2,
q3 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 &
LE q1,
q2,
P,
p1,
p2 &
LE q2,
q3,
P,
p1,
p2 holds
(Segment (P,p1,p2,q1,q2)) /\ (Segment (P,p1,p2,q2,q3)) = {q2}