let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment P,p1,p2,q1,q2 = { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) }
let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: Segment P,p1,p2,q1,q2 = { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) }
thus Segment P,p1,p2,q1,q2 c= { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } :: according to XBOOLE_0:def 10 :: thesis: { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } c= Segment P,p1,p2,q1,q2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Segment P,p1,p2,q1,q2 or x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } )
assume A1: x in Segment P,p1,p2,q1,q2 ; :: thesis: x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) }
then A2: x in R_Segment P,p1,p2,q1 by XBOOLE_0:def 4;
A3: x in L_Segment P,p1,p2,q2 by A1, XBOOLE_0:def 4;
A4: ex q being Point of (TOP-REAL 2) st
( q = x & LE q1,q,P,p1,p2 ) by A2;
ex p being Point of (TOP-REAL 2) st
( p = x & LE p,q2,P,p1,p2 ) by A3;
hence x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } by A4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } or x in Segment P,p1,p2,q1,q2 )
assume x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } ; :: thesis: x in Segment P,p1,p2,q1,q2
then A5: ex q being Point of (TOP-REAL 2) st
( q = x & LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) ;
then A6: x in R_Segment P,p1,p2,q1 ;
x in L_Segment P,p1,p2,q2 by A5;
hence x in Segment P,p1,p2,q1,q2 by A6, XBOOLE_0:def 4; :: thesis: verum