let C be Simple_closed_curve; :: thesis: C = Segment (W-min C),(W-min C),C
set X = { p where p is Point of (TOP-REAL 2) : ( LE W-min C,p,C or ( W-min C in C & p = W-min C ) ) } ;
A1: Segment (W-min C),(W-min C),C = { p where p is Point of (TOP-REAL 2) : ( LE W-min C,p,C or ( W-min C in C & p = W-min C ) ) } by JORDAN7:def 1;
thus C c= Segment (W-min C),(W-min C),C :: according to XBOOLE_0:def 10 :: thesis: Segment (W-min C),(W-min C),C c= C

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in C or e in Segment (W-min C),(W-min C),C )
assume A2: e in C ; :: thesis: e in Segment (W-min C),(W-min C),C
then reconsider p = e as Point of (TOP-REAL 2) ;
LE W-min C,p,C by A2, JORDAN7:3;
hence e in Segment (W-min C),(W-min C),C by A1; :: thesis: verum

end;

thus Segment (W-min C),(W-min C),C c= C by JORDAN16:10; :: thesis: verum