[\a/] <= a by INT_1:def 6;
then [\a/] < - 1 by TA1, XXREAL_0:2;
hence ( [\a/] is heavy & [\a/] is negative ) by TA1; :: thesis: verum