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;
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;
suppose ( q1 in Upper_Arc P & q2 in Lower_Arc P ) ; :: thesis: ( q1 in P & q2 in P )
hence ( q1 in P & q2 in P ) by A3, XBOOLE_0:def 3; :: thesis: verum
end;
suppose ( q1 in Upper_Arc P & q2 in Upper_Arc P ) ; :: thesis: ( q1 in P & q2 in P )
hence ( q1 in P & q2 in P ) by A3, XBOOLE_0:def 3; :: thesis: verum
end;
suppose ( q1 in Lower_Arc P & q2 in Lower_Arc P ) ; :: thesis: ( q1 in P & q2 in P )
hence ( q1 in P & q2 in P ) by A3, XBOOLE_0:def 3; :: thesis: verum
end;
end;