let P be non empty compact Subset of (); :: thesis: for q being Point of () 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 (); :: 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 () : ( LE q,p,P & LE p,q,P ) } by ;
then ex p being Point of () st
( p = x & LE q,p,P & LE p,q,P ) ;
hence x = q by ; :: thesis: verum
end;
assume A4: x = q ; :: thesis: x in Segment (q,q,P)
LE q,q,P by ;
then x in { p where p is Point of () : ( LE q,p,P & LE p,q,P ) } by A4;
hence x in Segment (q,q,P) by ; :: thesis: verum
end;
hence Segment (q,q,P) = {q} by TARSKI:def 1; :: thesis: verum