let P be non empty compact Subset of (TOP-REAL 2); :: thesis: for q being Point of (TOP-REAL 2) st P is being_simple_closed_curve & q in P & q <> W-min P holds
Segment q,q,P = {q}
let q be Point of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & q in P & q <> W-min P implies Segment q,q,P = {q} )
assume that
A1: P is being_simple_closed_curve and
A2: q in P and
A3: q <> W-min P ; :: thesis: Segment q,q,P = {q}
for x being set holds
( x in Segment q,q,P iff x = q )

proof

let x be set ; :: thesis: ( x in Segment q,q,P iff x = q )

hereby :: thesis: ( x = q implies x in Segment q,q,P )

assume x in Segment q,q,P ; :: thesis: x = q
then x in { p where p is Point of (TOP-REAL 2) : ( LE q,p,P & LE p,q,P ) } by A3, Def1;
then ex p being Point of (TOP-REAL 2) st
( p = x & LE q,p,P & LE p,q,P ) ;
hence x = q by A1, JORDAN6:72; :: thesis: verum

end;

assume A4: x = q ; :: thesis: x in Segment q,q,P
LE q,q,P by A1, A2, JORDAN6:71;
then x in { p where p is Point of (TOP-REAL 2) : ( LE q,p,P & LE p,q,P ) } by A4;
hence x in Segment q,q,P by A3, Def1; :: thesis: verum

end;

hence Segment q,q,P = {q} by TARSKI:def 1; :: thesis: verum