theorem :: XBOOLEAN:20

for p, q being boolean object holds p '&' (p <=> q) = p '&' q