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 object ; :: 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 object ; :: 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