theorem
for
P,
Q being
Subset of
(TOP-REAL 2) for
p1,
p2 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 &
P meets Q &
P /\ Q is
closed holds
(
First_Point (
P,
p1,
p2,
Q)
= Last_Point (
P,
p2,
p1,
Q) &
Last_Point (
P,
p1,
p2,
Q)
= First_Point (
P,
p2,
p1,
Q) )