the_unity_wrt addreal = 0 by Lm3, BINOP_1:def 8;