theorem :: EUCLID_7:51

for n being Element of NAT holds dim (REAL-US n) = n