for a, b, c, d being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st a <> b & P is_an_arc_of c,d & LE a,b,P,c,d holds
ex e being Point of (TOP-REAL 2) st
( a <> e & b <> e & LE a,e,P,c,d & LE e,b,P,c,d )