theorem :: MFOLD_2:23

for n being Nat holds RN_Base n is Basis of TOP-REAL n