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 set ; :: 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 by JORDAN5C:def 3; :: thesis: verum