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)
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;
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: verum