let C be Simple_closed_curve; :: thesis: 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); :: thesis: Segment (p,q,C) c= C
set S = Segment (p,q,C);
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in Segment (p,q,C) or e in C )
assume A1: e in Segment (p,q,C) ; :: thesis: 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 ; :: thesis: e in C

then Segment (p,q,C) = { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,C or ( p in C & p1 = W-min C ) ) } by JORDAN7:def 1;
then consider p1 being Point of (TOP-REAL 2) such that
A3: ( e = p1 & ( LE p,p1,C or ( p in C & p1 = W-min C ) ) ) by A1;

now :: thesis: ( LE p,p1,C implies p1 in C )

assume LE p,p1,C ; :: thesis: p1 in C
then ( p1 in Upper_Arc C or p1 in Lower_Arc C ) by JORDAN6:def 10;
hence p1 in C by A2; :: thesis: verum

end;

hence e in C by A3, SPRECT_1:13; :: thesis: verum

end;

suppose q <> W-min C ; :: thesis: e in C

then 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; :: thesis: verum

end;

end;