theorem :: XBOOLEAN:23

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