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