theorem :: BVFUNC_1:57

for x being boolean object holds FALSE <=> x = 'not' x ;