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 object holds
( x in Segment (q,q,P) iff x = q )

proof

let x be object ; :: 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:57; :: thesis: verum

end;

assume A4: x = q ; :: thesis: x in Segment (q,q,P)
LE q,q,P by A1, A2, JORDAN6:56;
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