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