theorem :: TOPDIM_2:21

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