theorem :: SIMPLEX2:26

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