let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
LE p1,p2,P,p1,p2
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 implies LE p1,p2,P,p1,p2 )
assume A1: P is_an_arc_of p1,p2 ; :: thesis: LE p1,p2,P,p1,p2
then p2 in P by TOPREAL1:1;
hence LE p1,p2,P,p1,p2 by A1, Th10; :: thesis: verum