let a, b be Real; :: thesis: ( a >= b implies (a -' b) + b = a )
assume a >= b ; :: thesis: (a -' b) + b = a
then a - b = a -' b by Th48, XREAL_0:def 2;
hence (a -' b) + b = a ; :: thesis: verum