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
consider x being Element of (Segment q1,q2,P) /\ (Segment q3,q4,P);
assume A7: (Segment q1,q2,P) /\ (Segment q3,q4,P) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then A8: x in Segment q1,q2,P by XBOOLE_0:def 4;
A9: 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 A10: q4 <> W-min P ; :: thesis: contradiction

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 A11: ex p2 being Point of (TOP-REAL 2) st
( p2 = x & LE q1,p2,P & LE p2,q2,P ) ;
x in { p1 where p1 is Point of (TOP-REAL 2) : ( LE q3,p1,P & LE p1,q4,P ) } by A9, A10, Def1;
then ex p1 being Point of (TOP-REAL 2) st
( p1 = x & LE q3,p1,P & LE p1,q4,P ) ;
then LE q3,q2,P by A1, A11, JORDAN6:73;
hence contradiction by A1, A3, A6, JORDAN6:72; :: thesis: verum

end;

end;