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 P & q2 in P )

let q1, q2 be Point of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & LE q1,q2,P implies ( q1 in P & q2 in P ) )

assume that

A1: P is being_simple_closed_curve and

A2: LE q1,q2,P ; :: thesis: ( q1 in P & q2 in P )

A3: (Upper_Arc P) \/ (Lower_Arc P) = P by A1, JORDAN6:50;

( q1 in P & q2 in P )

let q1, q2 be Point of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & LE q1,q2,P implies ( q1 in P & q2 in P ) )

assume that

A1: P is being_simple_closed_curve and

A2: LE q1,q2,P ; :: thesis: ( q1 in P & q2 in P )

A3: (Upper_Arc P) \/ (Lower_Arc P) = P by A1, JORDAN6:50;

per cases
( ( q1 in Upper_Arc P & q2 in Lower_Arc P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P ) )
by A2, JORDAN6:def 10;

end;