let A be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment (A,p1,p2,q1,q2) c= A
let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: Segment (A,p1,p2,q1,q2) c= A
Segment (A,p1,p2,q1,q2) = (R_Segment (A,p1,p2,q1)) /\ (L_Segment (A,p1,p2,q2)) by JORDAN6:def 5;
then ( R_Segment (A,p1,p2,q1) c= A & Segment (A,p1,p2,q1,q2) c= R_Segment (A,p1,p2,q1) ) by JORDAN6:20, XBOOLE_1:17;
hence Segment (A,p1,p2,q1,q2) c= A ; :: thesis: verum