theorem L724x: :: FUZZY_8:3

for a, x being Real holds a - |.x.| <= a