theorem :: XREAL_1:20

for a, b, c being Real holds
( a <= b + c iff a - b <= c ) by Lm18, Lm19;