let A be Subset of (TOP-REAL 2); 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); ( q in A implies q in R_Segment (A,p1,p2,q) )
assume
q in A
; 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; verum