theorem Th10:
for
P being non
empty compact Subset of
(TOP-REAL 2) for
q1,
q2,
q3 being
Point of
(TOP-REAL 2) st
P is
being_simple_closed_curve &
LE q1,
q2,
P &
LE q2,
q3,
P & ( not
q1 = q2 or not
q1 = W-min P ) & ( not
q2 = q3 or not
q2 = W-min P ) holds
(Segment (q1,q2,P)) /\ (Segment (q2,q3,P)) = {q2}