let P be non empty compact Subset of (TOP-REAL 2); 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); ( 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
; 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)) <> {}
; XBOOLE_0:def 7 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 A10:
q4 <> W-min P
;
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;
verum end;