set TR = TOP-REAL n;
set H = { q where q is Point of (TOP-REAL n) : for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] } ;
{ q where q is Point of (TOP-REAL n) : for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] } c= the carrier of (TOP-REAL n)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of (TOP-REAL n) : for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] } or x in the carrier of (TOP-REAL n) )
assume x in { q where q is Point of (TOP-REAL n) : for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] } ; :: thesis: x in the carrier of (TOP-REAL n)
then ex q being Point of (TOP-REAL n) st
( q = x & ( for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ) ) ;
hence x in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

then reconsider H = { q where q is Point of (TOP-REAL n) : for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] } as Subset of (TOP-REAL n) ;
take H ; :: thesis: for q being Point of (TOP-REAL n) holds
( q in H iff for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] )
let q be Point of (TOP-REAL n); :: thesis: ( q in H iff for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] )

hereby :: thesis: ( ( for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ) implies q in H )

assume q in H ; :: thesis: for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).]
then ex Q being Point of (TOP-REAL n) st
( q = Q & ( for i being Nat st i in Seg n holds
Q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ) ) ;
hence for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ; :: thesis: verum

end;

thus ( ( for i being Nat st i in Seg n holds
q . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] ) implies q in H ) ; :: thesis: verum