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)
set x = the 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: the Element of (Segment (q1,q2,P)) /\ (Segment (q3,q4,P)) in Segment (q1,q2,P) by XBOOLE_0:def 4;
A9: the Element of (Segment (q1,q2,P)) /\ (Segment (q3,q4,P)) 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 the Element of (Segment (q1,q2,P)) /\ (Segment (q3,q4,P)) 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 = the Element of (Segment (q1,q2,P)) /\ (Segment (q3,q4,P)) & LE q1,p2,P & LE p2,q2,P ) ;
the Element of (Segment (q1,q2,P)) /\ (Segment (q3,q4,P)) 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 = the Element of (Segment (q1,q2,P)) /\ (Segment (q3,q4,P)) & LE q3,p1,P & LE p1,q4,P ) ;
then LE q3,q2,P by A1, A11, JORDAN6:58;
hence contradiction by A1, A3, A6, JORDAN6:57; :: thesis: verum

end;

end;