theorem :: BINARI_6:31

for x, y, z being Element of BOOLEAN * st x in rng Nat2BL & y in rng Nat2BL & z in rng Nat2BL holds
(x + y) + z = x + (y + z)