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