theorem :: BVFUNC_1:64

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