theorem :: BVFUNC_1:58

for x being boolean object holds
( x <=> x = TRUE & 'not' (x <=> x) = FALSE ) by XBOOLEAN:125, XBOOLEAN:143;