let b, a be real number ; :: thesis: ( b <= a implies a -' b = a - b )
assume a >= b ; :: thesis: a -' b = a - b
then a - b >= 0 by Th50;
hence a -' b = a - b by XREAL_0:def 2; :: thesis: verum