theorem :: BVFUNC_1:53

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