theorem :: BINOP_2:3

the_unity_wrt addrat = 0 by Lm4, BINOP_1:def 8;