for n being Nat holds ind (TOP-REAL n) = n