[/a\] >= a by INT_1:def 7;
hence [/a\] is heavy by TA1, XXREAL_0:2; :: thesis: verum