let N be Nat; :: thesis: |.(0. (TOP-REAL N)).| = 0
thus |.(0. (TOP-REAL N)).| = |.(0* N).| by EUCLID:70
.= 0 by EUCLID:7 ; :: thesis: verum