let P be Subset of (TOP-REAL 2); :: thesis: for q being Point of (TOP-REAL 2) st P is being_simple_closed_curve & q in P holds

LE q,q,P

let q be Point of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & q in P implies LE q,q,P )

assume that

A1: P is being_simple_closed_curve and

A2: q in P ; :: thesis: LE q,q,P

A3: (Upper_Arc P) \/ (Lower_Arc P) = P by A1, Def9;

A4: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, Th50;

LE q,q,P

let q be Point of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & q in P implies LE q,q,P )

assume that

A1: P is being_simple_closed_curve and

A2: q in P ; :: thesis: LE q,q,P

A3: (Upper_Arc P) \/ (Lower_Arc P) = P by A1, Def9;

A4: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, Th50;

now :: thesis: ( ( q in Upper_Arc P & LE q,q,P ) or ( q in Lower_Arc P & not q in Upper_Arc P & LE q,q,P ) )

hence
LE q,q,P
; :: thesis: verumend;