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 & 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 & q2 <> q3 implies Segment (q1,q2,P) misses Segment (q3,(W-min P),P) )
assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q3,P and
A4: q1 <> W-min P and
A5: q2 <> q3 ; :: thesis: Segment (q1,q2,P) misses Segment (q3,(W-min P),P)
set x = the Element of (Segment (q1,q2,P)) /\ (Segment (q3,(W-min P),P));
assume A6: (Segment (q1,q2,P)) /\ (Segment (q3,(W-min P),P)) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then A7: the Element of (Segment (q1,q2,P)) /\ (Segment (q3,(W-min P),P)) in Segment (q1,q2,P) by XBOOLE_0:def 4;
the Element of (Segment (q1,q2,P)) /\ (Segment (q3,(W-min P),P)) in Segment (q3,(W-min P),P) by A6, XBOOLE_0:def 4;
then the Element of (Segment (q1,q2,P)) /\ (Segment (q3,(W-min P),P)) 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 A8: ex p1 being Point of (TOP-REAL 2) st
( p1 = the Element of (Segment (q1,q2,P)) /\ (Segment (q3,(W-min P),P)) & ( LE q3,p1,P or ( q3 in P & p1 = W-min P ) ) ) ;
q2 <> W-min P by A1, A2, A4, Th2;
then the Element of (Segment (q1,q2,P)) /\ (Segment (q3,(W-min P),P)) in { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } by A7, Def1;
then ex p3 being Point of (TOP-REAL 2) st
( p3 = the Element of (Segment (q1,q2,P)) /\ (Segment (q3,(W-min P),P)) & LE q1,p3,P & LE p3,q2,P ) ;
then LE q3,q2,P by A1, A4, A8, Th2, JORDAN6:58;
hence contradiction by A1, A3, A5, JORDAN6:57; :: thesis: verum