theorem Th4: :: RLAFFIN3:4

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