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 )

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

hence
Segment (q,q,P) = {q}
by TARSKI:def 1; :: thesis: verum
let x be object ; :: thesis: ( x in Segment (q,q,P) iff x = q )

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;hereby :: thesis: ( x = q implies x in Segment (q,q,P) )

assume A4:
x = q
; :: thesis: 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;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

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