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