(frac a) + (frac (- a)) = 1 by FRA;
hence ( not (frac a) + (frac (- a)) is zero & (frac a) + (frac (- a)) is trivial ) by NAT_2:def 1; :: thesis: verum