let P be Subset of (TOP-REAL 2); 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); R_Segment (P,p1,p2,q1) c= P
let x be object ; TARSKI:def 3 ( not x in R_Segment (P,p1,p2,q1) or x in P )
assume
x in R_Segment (P,p1,p2,q1)
; 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
; verum