let a be real number ; :: thesis: a -' a = 0
a - a = 0 ;
hence a -' a = 0 by XREAL_0:def 2; :: thesis: verum