for n being Nat
for X being object holds
( X is Subspace of REAL-NS n iff X is Subspace of TOP-REAL n )