let C be Simple_closed_curve; :: thesis: for p being Point of (TOP-REAL 2) st p in C holds
( p in Segment (p,(W-min C),C) & W-min C in Segment (p,(W-min C),C) )
let p be Point of (TOP-REAL 2); :: thesis: ( p in C implies ( p in Segment (p,(W-min C),C) & W-min C in Segment (p,(W-min C),C) ) )
A1: Segment (p,(W-min C),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;
assume A2: p in C ; :: thesis: ( p in Segment (p,(W-min C),C) & W-min C in Segment (p,(W-min C),C) )
then LE p,p,C by JORDAN6:56;
hence p in Segment (p,(W-min C),C) by A1; :: thesis: W-min C in Segment (p,(W-min C),C)
thus W-min C in Segment (p,(W-min C),C) by A2, A1; :: thesis: verum