:: deftheorem defines is_OSin JORDAN20:def 5 :
for P being Subset of (TOP-REAL 2)
for p1, p2, p being Point of (TOP-REAL 2)
for e being Real holds
( p is_OSin P,p1,p2,e iff ( P is_an_arc_of p1,p2 & p in P & p `1 = e & ex p7 being Point of (TOP-REAL 2) st
( LE p7,p,P,p1,p2 & ( for p8 being Point of (TOP-REAL 2) st LE p7,p8,P,p1,p2 & LE p8,p,P,p1,p2 holds
p8 `1 = e ) & ( for p4 being Point of (TOP-REAL 2) st LE p4,p7,P,p1,p2 & p4 <> p7 holds
( ex p5 being Point of (TOP-REAL 2) st
( LE p4,p5,P,p1,p2 & LE p5,p7,P,p1,p2 & p5 `1 > e ) & ex p6 being Point of (TOP-REAL 2) st
( LE p4,p6,P,p1,p2 & LE p6,p7,P,p1,p2 & p6 `1 < e ) ) ) ) ) );