now

let x be set ; :: thesis: ( x in { (y + b) where y, b is Point of (TOP-REAL n) : ( y in X & b in B ) } implies x in the carrier of (TOP-REAL n) )
assume x in { (y + b) where y, b is Point of (TOP-REAL n) : ( y in X & b in B ) } ; :: thesis: x in the carrier of (TOP-REAL n)
then consider y, b being Point of (TOP-REAL n) such that
A1: ( x = y + b & y in X & b in B ) ;
thus x in the carrier of (TOP-REAL n) by A1; :: thesis: verum

end;

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