let A be Subset of ; :: thesis: for p1, p2, q1, q2 being Point of holds Segment A,p1,p2,q1,q2 c= A
let p1, p2, q1, q2 be Point of ; :: 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:21, XBOOLE_1:17;
hence Segment A,p1,p2,q1,q2 c= A by XBOOLE_1:1; :: thesis: verum