let a, b be real number ; :: thesis: ( a >= b implies (a -' b) + b = a )
assume a >= b ; :: thesis: (a -' b) + b = a
then a - b = a -' b by Th235;
hence (a -' b) + b = a ; :: thesis: verum