let a, b be real number ; :: thesis: ( 0 <= a implies b - a <= b )
( 0 <= a implies b - a <= b - 0 ) by Th15;
hence ( 0 <= a implies b - a <= b ) ; :: thesis: verum