let P be Subset of (TOP-REAL 2); for q1, q2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q1,P holds
q1 = q2
let q1, q2 be Point of (TOP-REAL 2); ( P is being_simple_closed_curve & LE q1,q2,P & LE q2,q1,P implies q1 = q2 )
assume that
A1:
P is being_simple_closed_curve
and
A2:
LE q1,q2,P
and
A3:
LE q2,q1,P
; q1 = q2
A4:
Lower_Arc P is_an_arc_of E-max P, W-min P
by A1, Def9;
A5:
(Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)}
by A1, Def9;
A6:
Upper_Arc P is_an_arc_of W-min P, E-max P
by A1, Th50;
hence
q1 = q2
; verum