let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1 being Point of (TOP-REAL 2) holds R_Segment (P,p1,p2,q1) c= P
let p1, p2, q1 be Point of (TOP-REAL 2); :: thesis: R_Segment (P,p1,p2,q1) c= P
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R_Segment (P,p1,p2,q1) or x in P )
assume x in R_Segment (P,p1,p2,q1) ; :: thesis: x in P
then ex q being Point of (TOP-REAL 2) st
( q = x & LE q1,q,P,p1,p2 ) ;
hence x in P ; :: thesis: verum