let A be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q being Point of (TOP-REAL 2) st q in A holds
q in R_Segment (A,p1,p2,q)
let p1, p2, q be Point of (TOP-REAL 2); :: thesis: ( q in A implies q in R_Segment (A,p1,p2,q) )
assume q in A ; :: thesis: q in R_Segment (A,p1,p2,q)
then A1: LE q,q,A,p1,p2 by JORDAN5C:9;
R_Segment (A,p1,p2,q) = { q1 where q1 is Point of (TOP-REAL 2) : LE q,q1,A,p1,p2 } by JORDAN6:def 4;
hence q in R_Segment (A,p1,p2,q) by A1; :: thesis: verum