let P be non empty compact Subset of (TOP-REAL 2); :: thesis: for q1, q2, q3, q4 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P & q1 <> q2 & q2 <> q3 holds
Segment q1,q2,P misses Segment q3,q4,P
let q1, q2, q3, q4 be Point of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P & q1 <> q2 & q2 <> q3 implies Segment q1,q2,P misses Segment q3,q4,P )
assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q3,P and
A4: LE q3,q4,P and
A5: q1 <> q2 and
A6: q2 <> q3 ; :: thesis: Segment q1,q2,P misses Segment q3,q4,P
assume A7: (Segment q1,q2,P) /\ (Segment q3,q4,P) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
consider x being Element of (Segment q1,q2,P) /\ (Segment q3,q4,P);
A8: ( x in Segment q1,q2,P & x in Segment q3,q4,P ) by A7, XBOOLE_0:def 4;

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

suppose q4 = W-min P ; :: thesis: contradiction

then q3 = W-min P by A1, A4, Th2;
hence contradiction by A1, A3, A6, Th2; :: thesis: verum

end;

suppose q4 <> W-min P ; :: thesis: contradiction

then x in { p1 where p1 is Point of (TOP-REAL 2) : ( LE q3,p1,P & LE p1,q4,P ) } by A8, Def1;
then consider p1 being Point of (TOP-REAL 2) such that
A9: ( p1 = x & LE q3,p1,P & LE p1,q4,P ) ;
q2 <> W-min P by A1, A2, A5, Th2;
then x in { p2 where p2 is Point of (TOP-REAL 2) : ( LE q1,p2,P & LE p2,q2,P ) } by A8, Def1;
then consider p2 being Point of (TOP-REAL 2) such that
A10: ( p2 = x & LE q1,p2,P & LE p2,q2,P ) ;
LE q3,q2,P by A1, A9, A10, JORDAN6:73;
hence contradiction by A1, A3, A6, JORDAN6:72; :: thesis: verum

end;

end;