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) )

( 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)
end;

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

end;

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

end;