for P being non empty Subset of (TOP-REAL 2)
for p1, p2, p being Point of (TOP-REAL 2)
for e being Real st P is_S-P_arc_joining p1,p2 & p1 `1 < e & p in P & p `1 = e & not p is_Lin P,p1,p2,e holds
p is_Rin P,p1,p2,e