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