theorem :: BINARITH:11

for x, y, z being boolean object holds (x 'or' y) 'or' z = x 'or' (y 'or' z) ;