theorem :: BINARI_6:30

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