let P be non empty Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & p2 <> q1 holds
Segment (P,p1,p2,q1,p2) is_an_arc_of q1,p2
let p1, p2, q1 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & q1 in P & p2 <> q1 implies Segment (P,p1,p2,q1,p2) is_an_arc_of q1,p2 )
assume that
A1: P is_an_arc_of p1,p2 and
A2: q1 in P and
A3: p2 <> q1 ; :: thesis: Segment (P,p1,p2,q1,p2) is_an_arc_of q1,p2
LE q1,p2,P,p1,p2 by A1, A2, JORDAN5C:10;
hence Segment (P,p1,p2,q1,p2) is_an_arc_of q1,p2 by A1, A3, JORDAN16:36; :: thesis: verum