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