theorem Th23: :: TOPRNS_1:23

for N being Nat holds |.(0. (TOP-REAL N)).| = 0