let C be Simple_closed_curve; for p, q being Point of (TOP-REAL 2) holds Segment (p,q,C) c= C
let p, q be Point of (TOP-REAL 2); Segment (p,q,C) c= C
set S = Segment (p,q,C);
let e be object ; TARSKI:def 3 ( not e in Segment (p,q,C) or e in C )
assume A1:
e in Segment (p,q,C)
; e in C
(Upper_Arc C) \/ (Lower_Arc C) = C
by JORDAN6:50;
then A2:
( Upper_Arc C c= C & Lower_Arc C c= C )
by XBOOLE_1:7;
per cases
( q = W-min C or q <> W-min C )
;
suppose
q <> W-min C
;
e in Cthen
Segment (
p,
q,
C)
= { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,C & LE p1,q,C ) }
by JORDAN7:def 1;
then consider p1 being
Point of
(TOP-REAL 2) such that A4:
e = p1
and A5:
LE p,
p1,
C
and
LE p1,
q,
C
by A1;
(
p1 in Upper_Arc C or
p1 in Lower_Arc C )
by A5, JORDAN6:def 10;
hence
e in C
by A2, A4;
verum end;