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