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 <> p2 holds

not p2 in L_Segment (P,p1,p2,q)

let p1, p2, q be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & q <> p2 implies not p2 in L_Segment (P,p1,p2,q) )

assume that

A1: P is_an_arc_of p1,p2 and

A2: q <> p2 ; :: thesis: not p2 in L_Segment (P,p1,p2,q)

assume p2 in L_Segment (P,p1,p2,q) ; :: thesis: contradiction

then ex w being Point of (TOP-REAL 2) st

( p2 = w & LE w,q,P,p1,p2 ) ;

hence contradiction by A1, A2, Th55; :: thesis: verum

not p2 in L_Segment (P,p1,p2,q)

let p1, p2, q be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & q <> p2 implies not p2 in L_Segment (P,p1,p2,q) )

assume that

A1: P is_an_arc_of p1,p2 and

A2: q <> p2 ; :: thesis: not p2 in L_Segment (P,p1,p2,q)

assume p2 in L_Segment (P,p1,p2,q) ; :: thesis: contradiction

then ex w being Point of (TOP-REAL 2) st

( p2 = w & LE w,q,P,p1,p2 ) ;

hence contradiction by A1, A2, Th55; :: thesis: verum