let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q <> p1 holds
not p1 in R_Segment (P,p1,p2,q)
let p1, p2, q be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & q <> p1 implies not p1 in R_Segment (P,p1,p2,q) )
assume that
A1: P is_an_arc_of p1,p2 and
A2: q <> p1 ; :: thesis: not p1 in R_Segment (P,p1,p2,q)
assume p1 in R_Segment (P,p1,p2,q) ; :: thesis: contradiction
then ex w being Point of (TOP-REAL 2) st
( p1 = w & LE q,w,P,p1,p2 ) ;
hence contradiction by A1, A2, Th54; :: thesis: verum