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 ) )
assume A1: p in C ; :: thesis: ( p in Segment p,(W-min C),C & W-min C in Segment p,(W-min C),C )
A2: 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;
LE p,p,C by A1, JORDAN6:71;
hence p in Segment p,(W-min C),C by A2; :: thesis: W-min C in Segment p,(W-min C),C
thus W-min C in Segment p,(W-min C),C by A1, A2; :: thesis: verum