let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1 being Point of (TOP-REAL 2) holds L_Segment (P,p1,p2,q1) c= P

let p1, p2, q1 be Point of (TOP-REAL 2); :: thesis: L_Segment (P,p1,p2,q1) c= P

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L_Segment (P,p1,p2,q1) or x in P )

assume x in L_Segment (P,p1,p2,q1) ; :: thesis: x in P

then ex q being Point of (TOP-REAL 2) st

( q = x & LE q,q1,P,p1,p2 ) ;

hence x in P ; :: thesis: verum

let p1, p2, q1 be Point of (TOP-REAL 2); :: thesis: L_Segment (P,p1,p2,q1) c= P

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L_Segment (P,p1,p2,q1) or x in P )

assume x in L_Segment (P,p1,p2,q1) ; :: thesis: x in P

then ex q being Point of (TOP-REAL 2) st

( q = x & LE q,q1,P,p1,p2 ) ;

hence x in P ; :: thesis: verum