let P be Subset of the carrier of (TOP-REAL 2); :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) 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 (TOP-REAL 2); :: 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:59, JORDAN6:60;
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