theorem :: XBOOLEAN:50

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