{ p where p is Point of (TOP-REAL 2) : p `2 = s } c= the carrier of (TOP-REAL 2)

proof

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

end;

hence { p where p is Point of (TOP-REAL 2) : p `2 = s } is Subset of (TOP-REAL 2) ; :: thesis: verum