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 set ; :: 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:65;
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 and
A4: ( LE p,p1,C or ( p in C & p1 = W-min C ) ) by A1;

now

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, A4, SPRECT_1:15; :: 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
A5: e = p1 and
A6: LE p,p1,C and
LE p1,q,C by A1;
( p1 in Upper_Arc C or p1 in Lower_Arc C ) by A6, JORDAN6:def 10;
hence e in C by A2, A5; :: thesis: verum

end;

end;