for n being Nat holds
( TOP-REAL n is finite-dimensional & dim (TOP-REAL n) = n )