theorem :: BVFUNC_1:56

for x being boolean object holds TRUE <=> x = x ;