let P be Subset of ; :: thesis: for p1, p2, q1, q2 being Point of st P is_an_arc_of p1,p2 & p1 <> q1 & p2 <> q2 holds
( not p1 in Segment P,p1,p2,q1,q2 & not p2 in Segment P,p1,p2,q1,q2 )
let p1, p2, q1, q2 be Point of ; :: thesis: ( P is_an_arc_of p1,p2 & p1 <> q1 & p2 <> q2 implies ( not p1 in Segment P,p1,p2,q1,q2 & not p2 in Segment P,p1,p2,q1,q2 ) )
assume ( P is_an_arc_of p1,p2 & p1 <> q1 & p2 <> q2 ) ; :: thesis: ( not p1 in Segment P,p1,p2,q1,q2 & not p2 in Segment P,p1,p2,q1,q2 )
then A1: ( not p2 in L_Segment P,p1,p2,q2 & not p1 in R_Segment P,p1,p2,q1 ) by JORDAN6:74, JORDAN6:75;
Segment P,p1,p2,q1,q2 = (R_Segment P,p1,p2,q1) /\ (L_Segment P,p1,p2,q2) by JORDAN6:def 5;
hence ( not p1 in Segment P,p1,p2,q1,q2 & not p2 in Segment P,p1,p2,q1,q2 ) by A1, XBOOLE_0:def 4; :: thesis: verum