for n being Nat
for X being set holds
( X is Basis of TOP-REAL n iff X is Basis of REAL-NS n )