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