theorem Th9: :: XREAL_1:9

for a, b, c being Real holds
( a <= b iff a - c <= b - c )