now

let x be set ; :: thesis: ( x in { y where y is Point of (TOP-REAL n) : B + y c= X } implies x in the carrier of (TOP-REAL n) )
assume x in { y where y is Point of (TOP-REAL n) : B + y c= X } ; :: thesis: x in the carrier of (TOP-REAL n)
then ex q being Point of (TOP-REAL n) st
( x = q & B + q c= X ) ;
hence x in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

hence { y where y is Point of (TOP-REAL n) : B + y c= X } is Subset of (TOP-REAL n) by TARSKI:def 3; :: thesis: verum