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

proof

hence
{ q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } is Subset of (TOP-REAL 2)
; :: thesis: verum
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 } or x in the carrier of (TOP-REAL 2) )

assume x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ; :: thesis: x in the carrier of (TOP-REAL 2)

then ex q being Point of (TOP-REAL 2) st

( q = x & LE q1,q,P,p1,p2 ) ;

hence x in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;assume x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ; :: thesis: x in the carrier of (TOP-REAL 2)

then ex q being Point of (TOP-REAL 2) st

( q = x & LE q1,q,P,p1,p2 ) ;

hence x in the carrier of (TOP-REAL 2) ; :: thesis: verum