let n be Nat; :: thesis: |.(0. (TOP-REAL n)).| = 0
n in NAT by ORDINAL1:def 12;
hence |.(0. (TOP-REAL n)).| = 0 by TOPRNS_1:23; :: thesis: verum