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