let a, b be Real; :: thesis: ( 0 <= a implies b - a <= b )
( 0 <= a implies b - a <= b - 0 ) by Th13;
hence ( 0 <= a implies b - a <= b ) ; :: thesis: verum