{ q where q is Point of : LE q1,q,P,p1,p2 } c= the carrier of (TOP-REAL 2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of : LE q1,q,P,p1,p2 } or x in the carrier of (TOP-REAL 2) )
assume x in { q where q is Point of : LE q1,q,P,p1,p2 } ; :: thesis: x in the carrier of (TOP-REAL 2)
then ex q being Point of st
( q = x & LE q1,q,P,p1,p2 ) ;
hence x in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;

hence { q where q is Point of : LE q1,q,P,p1,p2 } is Subset of ; :: thesis: verum