theorem Th37: :: EUCLID_2:39

for n being Nat holds |.(0. (TOP-REAL n)).| = 0 by TOPRNS_1:23;