let P be non empty compact Subset of (TOP-REAL 2); :: thesis: for q1, q2, q3 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & q1 <> W-min P & q1 <> q2 & q2 <> q3 holds
Segment q1,q2,P misses Segment q3,(W-min P),P
let q1, q2, q3 be Point of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & q1 <> W-min P & q1 <> q2 & q2 <> q3 implies Segment q1,q2,P misses Segment q3,(W-min P),P )
assume A1: ( P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & q1 <> W-min P & q1 <> q2 & q2 <> q3 ) ; :: thesis: Segment q1,q2,P misses Segment q3,(W-min P),P
assume A2: (Segment q1,q2,P) /\ (Segment q3,(W-min P),P) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
consider x being Element of (Segment q1,q2,P) /\ (Segment q3,(W-min P),P);
A3: ( x in Segment q1,q2,P & x in Segment q3,(W-min P),P ) by A2, XBOOLE_0:def 4;
then x in { p1 where p1 is Point of (TOP-REAL 2) : ( LE q3,p1,P or ( q3 in P & p1 = W-min P ) ) } by Def1;
then consider p1 being Point of (TOP-REAL 2) such that
A4: p1 = x and
A5: ( LE q3,p1,P or ( q3 in P & p1 = W-min P ) ) ;
q2 <> W-min P by A1, Th2;
then x in { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } by A3, Def1;
then ex p3 being Point of (TOP-REAL 2) st
( p3 = x & LE q1,p3,P & LE p3,q2,P ) ;
then LE q3,q2,P by A1, A4, A5, Th2, JORDAN6:73;
hence contradiction by A1, JORDAN6:72; :: thesis: verum