theorem :: BVFUNC_1:62

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