set X = { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } ;

now :: thesis: for x being object st x in { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } holds

x in the carrier of (TOP-REAL n)

hence
{ y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } is Subset of (TOP-REAL n)
by TARSKI:def 3; :: thesis: verumx in the carrier of (TOP-REAL n)

let x be object ; :: thesis: ( x in { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } implies x in the carrier of (TOP-REAL n) )

assume x in { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } ; :: thesis: x in the carrier of (TOP-REAL n)

then consider y being Point of (TOP-REAL n) such that

A1: ( x = y & |(p,(y - q))| = 0 ) ;

thus x in the carrier of (TOP-REAL n) by A1; :: thesis: verum

end;assume x in { y where y is Point of (TOP-REAL n) : |(p,(y - q))| = 0 } ; :: thesis: x in the carrier of (TOP-REAL n)

then consider y being Point of (TOP-REAL n) such that

A1: ( x = y & |(p,(y - q))| = 0 ) ;

thus x in the carrier of (TOP-REAL n) by A1; :: thesis: verum