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 that
A1: P is being_simple_closed_curve and
A2: 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 A3: q2 <> W-min P ; :: thesis: q1 in Segment (q1,q2,P)
q1 in P by A1, A2, Th5;
then LE q1,q1,P by A1, JORDAN6:56;
then q1 in { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } by A2;
hence q1 in Segment (q1,q2,P) by A3, Def1; :: thesis: verum
end;
suppose A4: q2 = W-min P ; :: thesis: q1 in Segment (q1,q2,P)
q1 in P by A1, A2, Th5;
then LE q1,q1,P by A1, JORDAN6:56;
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 A4, Def1; :: thesis: verum
end;
end;
end;
per cases ( q2 <> W-min P or q2 = W-min P ) ;
suppose A5: q2 <> W-min P ; :: thesis: q2 in Segment (q1,q2,P)
q2 in P by A1, A2, Th5;
then LE q2,q2,P by A1, JORDAN6:56;
then q2 in { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } by A2;
hence q2 in Segment (q1,q2,P) by A5, Def1; :: thesis: verum
end;
suppose A6: 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 A2;
hence q2 in Segment (q1,q2,P) by A6, Def1; :: thesis: verum
end;
end;