:: deftheorem Def1 defines Segment JORDAN7:def 1 :
for P being non empty compact Subset of (TOP-REAL 2)
for q1, q2 being Point of (TOP-REAL 2) holds
( ( q2 <> W-min P implies Segment (q1,q2,P) = { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } ) & ( not q2 <> W-min P implies Segment (q1,q2,P) = { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } ) );