let P be non empty compact Subset of (TOP-REAL 2); :: thesis: for q1, q2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P holds
( q1 in Segment q1,q2,P & q2 in Segment q1,q2,P )
let q1, q2 be Point of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & LE q1,q2,P implies ( q1 in Segment q1,q2,P & q2 in Segment q1,q2,P ) )
assume A1: ( P is being_simple_closed_curve & LE q1,q2,P ) ; :: thesis: ( q1 in Segment q1,q2,P & q2 in Segment q1,q2,P )

hereby :: thesis: q2 in Segment q1,q2,P

per cases ( q2 <> W-min P or q2 = W-min P ) ;

suppose A2: q2 <> W-min P ; :: thesis: q1 in Segment q1,q2,P

q1 in P by A1, Th5;
then LE q1,q1,P by A1, JORDAN6:71;
then q1 in { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } by A1;
hence q1 in Segment q1,q2,P by A2, Def1; :: thesis: verum

end;

suppose A3: q2 = W-min P ; :: thesis: q1 in Segment q1,q2,P

q1 in P by A1, Th5;
then LE q1,q1,P by A1, JORDAN6:71;
then q1 in { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } ;
hence q1 in Segment q1,q2,P by A3, Def1; :: thesis: verum

end;

end;

end;

per cases ( q2 <> W-min P or q2 = W-min P ) ;

suppose A4: q2 <> W-min P ; :: thesis: q2 in Segment q1,q2,P

q2 in P by A1, Th5;
then LE q2,q2,P by A1, JORDAN6:71;
then q2 in { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } by A1;
hence q2 in Segment q1,q2,P by A4, Def1; :: thesis: verum

end;

suppose A5: q2 = W-min P ; :: thesis: q2 in Segment q1,q2,P

q2 in { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } by A1;
hence q2 in Segment q1,q2,P by A5, Def1; :: thesis: verum

end;

end;