theorem :: XBOOLEAN:123

for p, q being boolean object holds p => (p 'or' q) = TRUE