let n be natural Number ; :: thesis: n -' 0 = n
n -' 0 = n - 0 by XREAL_0:def 2
.= n ;
hence n -' 0 = n ; :: thesis: verum