reconsider b = frac a as non negative Real by INT_1:43;
b = |.b.| ;
hence frac a is light by INT_1:43; :: thesis: verum