for n being Nat holds ind (TOP-REAL n) <= n by Lm9;