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

proof

hence
{ p where p is Point of (TOP-REAL 2) : p `1 = s } is Subset of (TOP-REAL 2)
; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL 2) : p `1 = s } or x in the carrier of (TOP-REAL 2) )

assume x in { p where p is Point of (TOP-REAL 2) : p `1 = s } ; :: thesis: x in the carrier of (TOP-REAL 2)

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

( p = x & p `1 = s ) ;

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

end;assume x in { p where p is Point of (TOP-REAL 2) : p `1 = s } ; :: thesis: x in the carrier of (TOP-REAL 2)

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

( p = x & p `1 = s ) ;

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