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