theorem :: BINARITH:12

for x being boolean object holds x 'or' x = x ;