theorem :: BVFUNC_1:63

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