theorem :: TOPDIM_2:20

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