{ p where p is Point of (TOP-REAL 2) : P₁[p] } c= the carrier of (TOP-REAL 2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL 2) : P₁[p] } or x in the carrier of (TOP-REAL 2) )
assume x in { p where p is Point of (TOP-REAL 2) : P₁[p] } ; :: thesis: x in the carrier of (TOP-REAL 2)
then ex p being Point of (TOP-REAL 2) st
( p = x & P₁[p] ) ;
hence x in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;

hence { p where p is Point of (TOP-REAL 2) : P₁[p] } is Subset of (TOP-REAL 2) ; :: thesis: verum