( - 1 <= a & a <= 1 ) by Th2;

per cases then ( ( - 1 <= a & a < (- 1) + 1 ) or ( 0 <= a & a < 0 + 1 ) or a = 1 ) by XXREAL_0:1;

suppose ( - 1 <= a & a < (- 1) + 1 ) ; :: thesis: [\a/] is weightless

then [\a/] = - 1 by REAL_3:2;
hence [\a/] is weightless ; :: thesis: verum

end;

suppose ( 0 <= a & a < 0 + 1 ) ; :: thesis: [\a/] is weightless

hence [\a/] is weightless by REAL_3:2; :: thesis: verum

end;

suppose a = 1 ; :: thesis: [\a/] is weightless

hence [\a/] is weightless ; :: thesis: verum

end;

end;