theorem :: BVFUNC_1:55
for x, y, z being boolean object holds x 'nor' (y 'or' z) = 'not' ((x 'or' y) 'or' z) ;