theorem Th61: :: REAL_NS2:61

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