reconsider b = - c as positive non heavy Real ;
A1: |.a.| <= 1 by Def1;
A2: |.b.| <= 1 by Def1;
( a - b <= 1 - b & 1 - b <= 1 - 0 ) by A1, XREAL_1:9, XREAL_1:10;
then A3: a - b <= 1 by XXREAL_0:2;
A4: ( b - a <= 1 - a & 1 - a <= 1 - 0 ) by A2, XREAL_1:9, XREAL_1:10;

per cases ( a - b >= 0 or a - b < 0 ) ;

suppose a - b >= 0 ; :: thesis: not a + c is heavy

hence not a + c is heavy by A3, ABSVALUE:def 1; :: thesis: verum

end;

suppose a - b < 0 ; :: thesis: not a + c is heavy

then |.(a - b).| = - (a - b) by ABSVALUE:def 1;
hence not a + c is heavy by A4, XXREAL_0:2; :: thesis: verum

end;

end;