let P be non empty compact Subset of (TOP-REAL 2); for q1, q2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & q1 <> W-min P & q2 <> W-min P holds
not W-min P in Segment (q1,q2,P)
let q1, q2 be Point of (TOP-REAL 2); ( P is being_simple_closed_curve & q1 <> W-min P & q2 <> W-min P implies not W-min P in Segment (q1,q2,P) )
assume that
A1:
P is being_simple_closed_curve
and
A2:
q1 <> W-min P
and
A3:
q2 <> W-min P
; not W-min P in Segment (q1,q2,P)
A4:
Segment (q1,q2,P) = { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) }
by A3, Def1;
now not W-min P in Segment (q1,q2,P)A5:
Upper_Arc P is_an_arc_of W-min P,
E-max P
by A1, JORDAN6:def 8;
assume
W-min P in Segment (
q1,
q2,
P)
;
contradictionthen consider p being
Point of
(TOP-REAL 2) such that A6:
p = W-min P
and A7:
LE q1,
p,
P
and
LE p,
q2,
P
by A4;
LE q1,
p,
Upper_Arc P,
W-min P,
E-max P
by A6, A7, JORDAN6:def 10;
hence
contradiction
by A2, A6, A5, JORDAN6:54;
verum end;
hence
not W-min P in Segment (q1,q2,P)
; verum