theorem :: XREAL_1:19

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