theorem LM910: :: BINARI_6:38

for A, B being Element of Class EqBL2Nat holds A + B = B + A